How Room to Prove reads Lean

Lean is a language in which a computer checks every step of a proof. Mathlib is its library: hundreds of thousands of checked theorems.

Lean is written for the computer as much as for people. Room to Prove reads it back to you as mathematics.

A proof, two ways

In Lean:

theorem eq_of_deriv_eq_zero {f : ℝ → ℝ} {a b : ℝ} (hab : a < b)
    (hfc : ContinuousOn f (Icc a b)) (hfd : DifferentiableOn ℝ f (Ioo a b))
    (h0 : ∀ x ∈ Ioo a b, deriv f x = 0) : f a = f b := by
  obtain ⟨c, hc, hslope⟩ := exists_deriv_eq_slope f hab hfc hfd
  rw [h0 c hc, eq_div_iff (sub_ne_zero.mpr hab.ne')] at hslope
  linarith

In Room to Prove, word for word:

Theorem eq_of_deriv_eq_zero

Let f : ℝ → ℝ and a, b ∈ ℝ. Suppose a < b (hab), f is continuous on [a, b] (hfc), f is differentiable on (a, b) (hfd) and ∀x ∈ (a, b), f′(x) = 0 (h0). Then f(a) = f(b).

1. From Lagrange's Mean Value Theorem (applied to f, (hab), (hfc) and (hfd)), obtain c, hc and hslope. Now c ∈ ℝ, hc : c ∈ (a, b) and hslope : f′(c) = (f(b) − f(a)) / (b − a).
2. Rewrite in hslope using (h0) (applied to c and (hc)) and eq_div_iff (applied to sub_ne_zero.mpr hab.ne′). It becomes hslope : 0 · (b − a) = f(b) − f(a). Using sub_ne_zero and ne_of_gt.
3. This follows from the hypotheses by linear arithmetic. This completes the proof.

✓ proved in Lean

• (hab), (hfc) are the author's labels for each assumption.
• Lagrange's Mean Value Theorem is Mathlib's own name for the theorem it uses. Click it to see it.
• "continuous" is a link too.

How it works

1. Lean reads it. The app never reads Lean itself. It asks Lean, which already knows every name, assumption and step.

2. Rules turn it into words. A variable becomes "Let …". An assumption becomes "Suppose …". The goal becomes "Then …". IsOpen s becomes "s is open". No AI is involved: the same proof always reads the same way.

3. Formulas are typeset. Each formula is built from Lean's meaning, not its text. So the app can print it as a textbook does:

• notation: Aut(E/F), the fixed field Eᴴ;
• ⊥ as what it means: F, {0} or ∅;
• natural numbers honestly: n / 2 rounds down, so it shows ⌊n/2⌋;
• a name with no symbol yet is shown by name, with its meaning below.

4. You choose the pace. Five views: Read, Steps, Step through, Narrative and Source. A step that ran automation can open to show what it did.

A page for every name

Every theorem and definition has a page:

• what it says;
• how it is proved;
• what it rests on;
• the names it uses, each a link;
• what the library proves about it.

What you can trust

Lean someone else wrote, like the assistant's, runs in a sandbox: no network, no access to your files.

What it won't do

• Tell you why. It says what each step does. Why is yours to think about.
• Promise Lean says what the book says. It shows the differences it can see. The last word is yours.
• Know every symbol yet. More than a third of Mathlib's 249,732 theorems read with every name as a symbol. Over nine in ten read fully with the meanings shown below them.

Questions

Do I need to know Lean? No.

Can I see the Lean? Yes, in Source, and on every page.

Does an AI decide if a proof is right? No. Only Lean decides.

A reading looks wrong? Press Tell us under it, on its page. Or write to developer@gghomology.com.au.

What is the ↑? A conversion between number systems that changes the meaning, shown so nothing is hidden. It is also shown when an equation would read x = x without it: there it marks an object seen as another kind, such as a subgroup seen as a set.

Why does a page say "Both sides read"? Some lemmas of the library say that two ways Lean writes one thing agree. A reading shows both the same way, so the equation looks like x = x. The page then says what tells the sides apart, in Lean's own words: "Both sides read . Lean writes them two ways: ⊥ and ∅." It is the one place a reading quotes Lean.

What is "(for m)"? The structure the statement means. It may be one the author named, such as a σ-algebra m, or one built for the purpose, such as an induced topology. It is not the usual one.

A few words