Lean Prover
Hey, welcome back to my blog! It’s been a minute since I last posted, but I’m back with something I’ve been pretty excited about lately. Today, I’m writing about the Lean theorem prover — it’s become pretty relevant with some recent changes in my life, and I thought it’d be cool to share. I recently started contributing to a project called Project Numina, where we formalize a wide range of math competition problems, from AMC to AIME level. The long-term goal is to eventually tackle IMO problems as well. It’s been an awesome opportunity to sharpen my skills and dive deeper into Lean. In this post, I’ll show you some of the neat things you can do with the Lean theorem prover and share a few resources that helped me learn Lean 4.
The first cool thing I want to highlight is formalizing mathematical proofs in Lean. You’ve seen how geometric theorems and propositions can be proven step-by-step, starting from a set of basic axioms. In Lean, you can do exactly the same — except with a high degree of precision and automation. By formalizing these proofs, we ensure that every logical step is verified and there’s no room for error, making the entire process not just rigorous, but also reproducible.
Let's look at an example. In the set of real numbers, or more specifically, in the group of real numbers under the binary operation of addition, we know that for every $x$, there exists a $y$ such that $x + y = 0$. A standard pencil-and-paper proof goes like this: Let $x \in \mathbb{R}$ be arbitrary. Set $y = -x$. Then $y \in \mathbb{R}$, and we have $x + y = 0$. Hence, for every $x$, there exists a $y$ such that $x + y = 0$. In Lean 4, we can formalize this proof as follows:
import Mathlib.Data.Real.Basic
theorem forall_x_exists_y_add_x_eq_zero : ∀ x : ℝ, ∃ y : ℝ, x + y = 0 := by
intro x
use -x
ring
This proof is an example of a tactic proof in Lean 4. The intro tactic introduces an arbitrary $x\in \mathbb{R}$. The use tactic gives a witness to $x + y = 0$ which is $y = -x$. Finally, the ring tactic finishes the proof by showing $x + (-x) = 0$. There are various tactics tailored for different purposes. I will discuss them in a future post.
Now you might be wondering what Mathlib.Data.Real.Basic stands for. Mathlib is Lean's library of various axiomatizations of theories and different proofs of theorems. Importing Mathlib.Data.Real.Basic gives us the basic facts about the real numbers to work with. Let's look at an example.
import Mathlib
theorem sum_of_evens_is_even {a b : ℕ} (ha : Even a) (hb : Even b) : Even (a + b) := by
exact Even.add ha hb
This theorem says that if $a$ and $b$ are even numbers in $\mathbb{N}$, then $a + b$ is an even number as well. The clauses ha : Even b and hb : Even b say that ha and ha are witnesses of the facts that $a$ is an even number and $b$ is an even number respectively. Notice that we have used a Mathlib theorem directly which is Even.add that says the sum of two even numbers is even. The exact tactic finishes the proof by taking the witness ha and hb.
Here are some problems that I formalized for Project Numina.
import Mathlib
set_option exponentiation.threshold 5000
/-Let f be a function with the following properties
(i) f(1) = 1 and
(ii) f(2n)= n ⬝ f(n) for any positive integer n.
What is the value of f(2^100)?
(A)1 (B)2^99 (C)2^100 (D)2^4950 (E)2^9999
-/
theorem algebra_95206 {f : ℕ → ℕ}
(h1 : f 1 = 1) (h2 : ∀ n > 0, f (2 * n) = n * f n) : f (2 ^ 100) = 2 ^ 4950 := by
have h : ∀ n : ℕ, f (2^n) = 2^((n-1) * n / 2) := by
intro n
induction n with
| zero =>
-- Base case: f(2^0) = f(1) = 1
rw [pow_zero]
--a^0 =1 for all a
exact h1
-- uses h1
| succ n ih =>
-- inductive step
calc
f (2 ^ (n + 1))
= f (2 * 2 ^ n) := by
rw [pow_succ, mul_comm]
_ = (2 ^ n) * f (2 ^ n) := by
apply h2
--uses the assumption h2
apply pow_pos
--shows 2>0
norm_num
--normalizes numerical expressions
_ = (2 ^ n) * (2 ^ ((n - 1) * n / 2)) := by
rw [ih]
--uses the inductive hypothesis
_ = 2 ^ (n + ((n - 1) * n / 2)) := by
ring_nf
--simplifying using ring_nf
_ = 2 ^ (((n + 1 - 1) * (n + 1)) / 2) := by
congr
--ensures both sides are structurally same
symm
nth_rewrite 1 [mul_comm]
--apply tactic to 1st occurrence etc
nth_rewrite 2 [mul_comm]
nth_rewrite 2 [add_comm]
apply Nat.div_eq_of_eq_mul_right
--expresses division in form of multiplication
simp
--simplifies expression
rw [mul_add]
--expands product over addition
cases n with
--case analysis
| zero => simp
| succ n =>
simp
have : 2 * ((n + 1) * n / 2) = (n+1) * n := by
nth_rewrite 1 [mul_comm]
--Swap multiplication order in first occurrence
refine Nat.div_two_mul_two_of_even ?_
--property that division by 2 is valid when even
refine Nat.even_mul.mpr ?_
--`(n + 1) * n` is even
by_cases H : Even n
--either `n` is even or it is odd
· tauto
· left
exact Nat.even_add_one.mpr H
--if n is odd then n+1 is even
rw [this]
--rewrite using proven equality
linarith
--finishes goal
exact h 100
import Mathlib
/- 10.2. Given numbers $a, b, c$. It is known that for any $x$ the inequality
$$
a x^{2}+b x+c \geqslant b x^{2}+c x+a \geqslant c x^{2}+a x+b
$$
holds. Prove that $a=b=c$. -/
theorem inequalities_143807 (a b c : ℝ)
(h : ∀ x : ℝ, a * x^2 + b * x + c ≥ b * x^2 + c * x + a ∧ b * x^2 + c * x + a ≥ c * x^2 + a * x + b) :
a = b ∧ b = c := by
--Using `x = 0` we get two inequalities `c ≥ a` and `a ≥ b`.
have h0 := h 0
rcases h0 with ⟨h1, h2⟩
have hcgea : c ≥ a := by linarith [h1]
have hageb : a ≥ b := by linarith [h2]
--Using `x = -1` we get the inequality `a ≥ c`.
have hneg1 := h (-1)
rcases hneg1 with ⟨h3, h4⟩
have h3_1 : a - b + c ≥ b - c + a := by linarith [h3]
have h4_1 : b - c + a ≥ c - a + b := by linarith [h4]
have h4_1_1 : a ≥ c := by linarith [h4_1]
--We get `a = c` using `c ≥ a` and `a ≥ c`.
have haeqc : a = c := by
apply le_antisymm
exact hcgea
exact h4_1_1
--We are almost done. We get `b ≥ c` using `x = -2`.
--Then we use the fact `a = c` to end the proof.
have hneg2 := h (-2)
rcases hneg2 with ⟨h5, h6⟩
have h5_1 : 4 * a - 2 * b + c ≥ 4 * b - 2 * c + a := by linarith [h5]
have h6_1 : 4 * b - 2 * c + a ≥ 4 * c - 2 * a + b := by linarith [h6]
have h6_1_1 : 3 * b - 6 * c + 3 * a ≥ 0 := by linarith [h6_1]
rw [haeqc] at h6_1_1
have h6_1_2 : 3 * b ≥ 3 * c := by linarith [h6_1_1]
have hcleb : c ≤ b := by linarith [h6_1_2]
have hblec : b ≤ c := by
rw [haeqc] at hageb
exact hageb
have hbeqc : b = c := by exact le_antisymm hblec hcleb
rw [←haeqc] at hcleb
have haeqb : a = b := by exact le_antisymm hcleb hageb
exact ⟨haeqb, hbeqc⟩
I was introduced to the Lean theorem prover using a nice and fun game called the Natural Number Game. It's a great way to learn some Lean syntax and various useful tactics. There are more fun games about set theory and logic as well. You can find them here.
After familiarizing myself with the basics of Lean, I used the free book Mathematics in Lean. It's a nice online book that introduced me to do mathematics in Lean 4. The other free online book is Theorem Proving in Lean. I gained a lot by reading these two books in parallel. In addition to these books, I followed Kevin Buzzard's Formalizing Mathematics course as well.
Just as we use set theory as a foundation to build mathematics, we can also use type theory for the same purpose. Lean is built on a type theory known as dependent type theory. In this blog post, I won’t go into types or dependent types—but it’s useful to know that dependent types are the foundation of how Lean works.
On the meta-side of Lean, there are communities working on creating tactics and that'll help automate mathematical proofs. This adds to the list of benefits of Lean being an interactive theorem prover. Such tactics will allow users to write clear and concise proofs. Here is a nice talk by Jason Rute discussing the meta aspects of Lean.
As I mentioned before, Mathlib is Lean's library of tactics and theorems. Anybody can contribute to Mathlib by proving theorems and communicating them to the Lean community. Another great resource is Lean community's Zulip Chat, where we can ask questions and get help from the experts.
In the next post, I’ll explore some powerful tactics commonly used in Lean for proving theorems. See you soon!