Room to Prove
Docs Control and automate

Lean

Lean checks every step of a proof. Room to Prove uses Lean 4 and Mathlib, its library, and reads each proof back to you in words.

How the reading is made: How Room to Prove reads Lean.

Three ways Lean appears

In a lesson You write You get
A linked statement lean="name" module="Module" Lean's reading, and its page
A Lean block a lean block a checked file, with five views
A draft's Lean a lean block in your draft a Check button

A Lean block

Lean
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Tactic.Ring

theorem sum_first (n : ℕ) : 2 * (∑ i ∈ Finset.range (n + 1), i) = n * (n + 1) := by
  induction n with
  | zero => simp
  | succ k ih =>
    rw [Finset.sum_range_succ, mul_add, ih]
    ring

Here, press Check to have Lean check it. Then Read shows it as mathematics: "Let n ∈ ℕ. Then …", and a proof by induction.

Badges

Badge Means
✓ proved in Lean rests only on Lean's standard axioms
checked by Lean a block you checked: no errors, all proved
depends on sorry part of the proof is missing
uses axioms: … rests on an axiom of its own: not proved
re-check independently check again with a second checker

A declaration's page

Every name in Lean has a page:

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

Press ⌘K. Type a name, words, or symbols like "a < b → a ≤ b".

Lean someone else wrote

Running Lean runs code. So Lean you didn't write runs in a sandbox:

  • no network;
  • no access to your files;
  • stopped after three minutes.

Your own Lean library

A plugin can bring a Lean library, public or private. The app builds it in the sandbox. Then your drafts can import it. See Plugins.

For agents

  • lean_check: check a file in the sandbox, and read it back.
  • mathlib_search: find names by words.
  • mathlib_decl: read one declaration.

The assistant links a statement to Lean only after reading it.

PreviousPython