Concolic testing

 Sequence-Based Incremental Concolic Testing of RTL Models

MIT 6.824 Distributed Systems

MX and vector world

 VMXDOTP: A RISC-V Vector ISA Extension for Efficient Microscaling (MX) Format Acceleration

Takeaways:

1. Microscaling (MX) data formats, based on block floating-point (BFP) representations, have emerged as a promising solution to reduce data volumes while preserving accuracy. However, MX semantics are poorly aligned with vector execution: block scaling and multi-step mixed-precision operations break the regularity of vector pipelines, leading to underutilized compute resources and performance degradation. 

2. As bitwidths decrease, preserving model accuracy becomes increasingly challenging due to the reduced dynamic range and precision [1]. To alleviate this trade-off, block-scaled data formats have emerged as a compelling solution. By associating a shared scale factor with a block of low-bitwidth elements, these formats preserve high dynamic range while retaining the benefits of a compact representation

3. While the memory savings of MX formats are a direct consequence of their compact design, their computational benefits are often overlooked. MX quantization is frequently treated as a storage-only compression approach to alleviate memory bottlenecks, requiring decompression to wider formats before computation [4], [5]

Math

 Linear Algebra

Mathematics for computer science from MIT course

Undergrad amth in lean

the-deep-link-equating-math-proofs-and-computer-programs - "Curry-Howard correspondence posits that two concepts from computer science (types and programs) are equivalent, respectively, to propositions and proofs — concepts from logic."

Towards a Lean proof of Fermat’s Last Theorem

https://x.com/zk_monk/status/2030305129493049748 - Everything you wanted to know about Maths

Books on Algorithms

 

Connecting to Books on Algorithms

If you want a book that collects these algorithms and explains their reasoning, here are the most relevant:

🔹 The Algorithm Design Manual — Steven Skiena slides Introduction to Algorithm Design

• Organizes algorithms by problem type

• Emphasizes design patterns (very close to modes of thinking)

• Includes stories behind each major algorithm

🔹 Introduction to Algorithms — Cormen, Leiserson, Rivest, Stein (CLRS)  Introduction to Algorithms

• Covers most of the “10 foundational algorithms”

• Each algorithm is presented with:

  • Description

  • Correctness proof (invariants)

  • Complexity analysis (optimization)

🔹 Concrete Mathematics — Graham, Knuth, Patashnik Concrete Mathematics

• Focuses on mathematical foundations underlying algorithms

• Shows how proofs and thinking modes map to efficient computation

five core modes of mathematical thinking

 most discoveries come from a small number of thinking patterns. These patterns generate both algorithms and theorems.

Below are five core modes of mathematical thinking that produce a huge fraction of results in mathematics and computer science.

---

1. Decomposition (Break the Problem Apart)

Idea: break a difficult problem into smaller simpler pieces.

This is one of the most powerful reasoning tools.

Example algorithm:

• Merge sort

How it works:

big problem
   ↓
split into smaller problems
   ↓
solve each
   ↓
combine answers

This idea appears everywhere:

• divide-and-conquer algorithms

• mathematical induction proofs

• dynamic programming

Many complex algorithms are just repeated decomposition.

---

2. Invariants (What Never Changes)

An invariant is something that stays constant during a process.

Example:
Euclidean algorithm

Key invariant:

$$gcd(a,b) = gcd(b, a \bmod b)$$

Even though the numbers change, the gcd remains the same.

Invariant thinking appears in:

• loop correctness proofs

• puzzle solving

• game theory

• algorithm design

Many elegant proofs rely on discovering one hidden invariant.

---

3. Symmetry

Symmetry reduces complexity because identical situations behave the same.

Example theorem:

Pythagorean theorem

Many proofs exploit symmetry of shapes.

Symmetry also appears in:

• physics laws

• group theory

• graph algorithms

Recognizing symmetry often collapses huge problems into small ones.

---

4. Recursion / Self-Reference

A structure defined in terms of itself.

Example algorithm:

• Quicksort

Example recursive idea:

solve(n):
   solve(n-1)

Examples in mathematics:

• factorial definition

• Fibonacci sequence

• fractals

• recursive data structures

Recursion allows infinite structures to be described with finite rules.

---

5. Optimization (Best Possible Solution)

Many problems ask:

What is the best possible outcome?

Examples:

• shortest path

• minimum cost

• maximum profit

Example algorithm:

• Dijkstra's algorithm

Optimization thinking appears in:

• operations research

• machine learning

• economics

• logistics

It often leads to greedy algorithms or dynamic programming.

---

The Deep Pattern

Most algorithms and theorems combine these ideas.

Example:

Shortest path algorithms use:

• decomposition

• invariants

• optimization

Sorting algorithms use:

• recursion

• decomposition

Proofs often combine:

• invariants

• symmetry

---

A Mental Toolkit

You can think of mathematical creativity like this:

Decompose the problem
Look for invariants
Use symmetry
Apply recursion
Optimize the result

These five tools generate huge portions of mathematics and algorithms.

---

✅ Interesting observation

Many of the deepest open problems — like
P versus NP problem — revolve around understanding how these patterns interact in computation.

Proof, Theorem and ALgorithm

 Here’s a roadmap of books and university‑level courses that are great for starting and deepening your journey into proof thinking, theorems, and algorithmic thinking — from beginner to advanced.

---

📘 Introductory Books (Building Proof & Logic Skills)

🔹 How to Think Like a Mathematician — Kevin Houston

A gentle guide to learning mathematical language and basic proof strategies. Great for beginners transitioning to formal math.

🔹 Book of Proof — Richard Hammack

Designed specifically to teach how to read and write proofs, with lots of examples and exercises.

🔹 How to Prove It — Daniel J. Velleman

Structured proof techniques — induction, contradiction, cases — ideal for writing your own proofs.

🔹 The Art of Problem Solving / Problem-Solving Strategies — Paul Zeitz / Arthur Engel

Not just proof methods but thinking like a mathematician and tackling rich problems. (Commonly recommended on math forums listing proof books.)

📚 Other accessible choices

• Mathematical Thinking: Problem‑Solving and Proofs — D’Angelo & West

• How to Read and Do Proofs — Daniel Solow

These all help you learn to think like a mathematician and understand why proofs matter.

---

📗 Discrete Mathematics & Algorithm Foundations

These texts are standard in CS programs because they mix proofs, logic, and algorithm thinking:

🔹 Discrete Mathematics and Its Applications — Kenneth Rosen

Covers logic, proof techniques, sets, combinatorics, graph theory and more — excellent for algorithmic thinking.

🔹 Concrete Mathematics — Graham, Knuth & Patashnik

A classic blend of continuous and discrete math used in analysis of algorithms.

🔹 Courses covering discrete math & proofs

• Introduction to Discrete Mathematics for Computer Science (Coursera) — includes logic, induction, recursion, invariants, and proofs connected with algorithms.

• Mathematical Thinking in Computer Science (Coursera) — part of the discrete specialization; focuses on proof, logic, algorithm design, and reasoning.

---

📙 Algorithm & Theory Classics

Once you’re comfortable with proofs and discrete math, these books take you deeper into algorithm design and correctness:

📌 Introduction to Algorithms — Cormen, Leiserson, Rivest & Stein (a.k.a. CLRS)

The standard algorithms text; formal and proof‑oriented, with many correctness proofs.

📌 The Algorithm Design Manual — Steven Skiena

More intuitive, with lots of design patterns and problem‑solving emphasis (less formal, but great practice).

📌 Algorithms — Robert Sedgewick & Kevin Wayne

Accessible and thorough, with implementations and analysis.

---

📘 Advanced Theoretical Paths

If you love proofs and want to go beyond basics:

🔹 Combinatorics: The Rota Way – (Advanced text, more abstract)

A graduate level combinatorics book packed with deep theorems and proof techniques.

🔹 Formal logic & proof theory texts

Topics like sequent calculus and formal proof systems sit between math and CS and help develop deep rigor.

---

🎓 University & Online Courses

Here are structured paths you can take:

🧠 Proof & Logic (for beginners)

• Intro to Mathematical Thinking / Proof Techniques (many universities offer these as “bridge” courses)

• Discrete Mathematics (widely offered for CS majors)

📊 Algorithms & Theoretical CS

• Introduction to Algorithms (often two semesters: design and analysis)

• Data Structures & Algorithms (proofs of correctness and complexity)

🧪 Deeper Into Theory

• Computability & Complexity (why some problems can or can’t be solved efficiently)

• Proof Assistants / Formal Verification (Lean, Coq, Isabelle)

GitHub lists like awesome‑theoretical‑computer‑science collect many courses and lecture notes in math/CS theory if you want organized references.

---

🧠 Tips for Sequencing Your Learning

1. Start with proof books — Hammack, Velleman, Houston

2. Move into discrete math / logic — Rosen, Concrete Math

3. Take algorithm design seriously — CLRS, Skiena

4. Explore advanced theory or formal systems if you want rigor like in research

harvard

 Vijay Janapa Reddi just put the entire ML Systems (CS249r)

Book - https://mlsysbook.ai/book/

https://github.com/harvard-edge/cs249r_book

Philosophy of Computer science book

AI Researcher Links Abstract Thinking to Body's Physical Mapping

Is Mathematics obsolete?

https://leodemoura.github.io/blog/2026/02/28/when-ai-writes-the-worlds-software.html

Discovering New Theorems via LLMs with In-Context Proof Learning in Lean

https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/ - linarith, library search tactic

Lean for the curious mathematician

To be a quant