Version 0.1.0 · Free

Room to Prove

Mathematics you can read, run and test.

A free desktop app to support learning mathematics.

Lean proofs, read as mathematics.
An AI assistant.
Lessons with live figures.
Python and exact computation.

Download free Read the docs

For macOS, Windows version coming soon.

A lesson on the Mean Value Theorem, with a live figure

Lean, read as mathematics

Room to Prove parses Lean with gradually refined rules and renders it in words.

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

Theorem eq_of_deriv_eq_zero✓ proved in Lean

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).

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).
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.
This follows from the hypotheses by linear arithmetic. This completes the proof.