kim@lean:~$ cat posts/2026·10·30.md

All 100 theorems in Lean

2026·10·30 [lean]

Freek Wiedijk has for many years maintained a list of 100 significant theorems in mathematics, and kept track of which interactive theorem proving languages have checked proofs of these theorems.

For the first time, a single language now has proofs of all 100 theorems: Lean!

And I'm very pleased to report that the 100th theorem completed in Lean was a strong formulation of Green's theorem, which landed in Tau Ceti, the library of all mathematics that we're autoformalizing with the Lean FRO and Mathlib Initiative.

Here is the statement in Lean:

theorem green_ac_index_one {γ : ℝ → ℂ} {a b : ℝ} {U : Set ℂ} {P Q : ℂ → ℝ}
    (hab : a < b) (hγ : AbsolutelyContinuousOnInterval γ a b) (hclosed : γ a = γ b)
    (hU : IsOpen U) (hregion : filledHull (γ '' uIcc a b) ⊆ U)
    (hP : ContDiffOn ℝ 1 P U) (hQ : ContDiffOn ℝ 1 Q U)
    (hindex : ∀ z ∈ filledHull (γ '' uIcc a b) \ (γ '' uIcc a b),
      Contour.windingNumber γ a b z = 1) :
    IntervalIntegrable (circulationFun P Q γ) volume a b ∧
      IntegrableOn (curl P Q) (filledHull (γ '' uIcc a b) \ (γ '' uIcc a b)) ∧
      (∫ t in a..b, circulationFun P Q γ t) =
        ∫ z in filledHull (γ '' uIcc a b) \ (γ '' uIcc a b), curl P Q z

The curve is only required to be absolutely continuous and closed, with winding number one throughout the bounded complementary region. There is no simplicity or finite-component hypothesis, and integrability of both sides is part of the conclusion.

Source · documentation