Welcome to Proofs and Intuitions! This is a blog about mathematics, formal verification, and the ideas that connect them.

A Bit of Mathematics

Let’s start with something beautiful. The most famous equation in physics is probably Einstein’s mass-energy equivalence: $E = mc^2$. But in pure mathematics, Euler’s identity takes the crown:

\[e^{i\pi} + 1 = 0\]

This single equation connects five fundamental constants: $e$, $i$, $\pi$, $1$, and $0$. Truly remarkable!

Here’s another classic—the quadratic formula. For any equation of the form $ax^2 + bx + c = 0$, the solutions are:

\[x = \frac{-b \pm \sqrt{b^2 - 4ac}}{2a}\]

Lean 4: Theorem Proving

One of the exciting developments in modern mathematics is the use of proof assistants like Lean. These tools allow us to write mathematical proofs that can be mechanically verified by a computer.

Proving the GCD algorithm correct in Lean with VSCode VSCode with Lean 4: proving correctness of the Euclidean GCD algorithm. The InfoView panel on the right shows the current proof state with three goals remaining.

Here’s a simple example. In Lean 4, we can define natural number addition and prove basic properties. For instance, we can express that 0 + n = n using the Nat.zero_add theorem.

A simple inline reference: the term Nat.succ n represents the successor of n, i.e., n + 1.

Here’s a small Lean 4 proof that addition is commutative:

theorem add_comm (n m : Nat) : n + m = m + n := by
  induction n with
  | zero => simp [Nat.zero_add, Nat.add_zero]
  | succ n ih => simp [Nat.succ_add, Nat.add_succ, ih]

And here’s a proof that demonstrates the associativity of addition:

theorem add_assoc (a b c : Nat) : (a + b) + c = a + (b + c) := by
  induction a with
  | zero => rfl
  | succ a ih => simp [Nat.succ_add, ih]

The Joy of Discovery

There’s a special feeling when a proof finally clicks—when the pieces fall into place and you see why something must be true, not just that it is true.

Math is beautiful

That moment of clarity is what this blog is about. We’ll explore proofs, develop intuitions, and hopefully have some fun along the way.

Stay tuned for more!