From problem to proof.
Verified by Lean.

Describe a problem or paste a Lean theorem. Lean4Proof finds the answer, writes the proof and typesets the solution. Every step is checked by Lean.

Watch the demo
Lean4Proof — Euclid’s theoremProved
A finished run of Euclid’s theorem: the Lean verdict Proved, the checked statement, the axioms, the statement review and the solution PDF.A finished run of Euclid’s theorem: the Lean verdict Proved, the checked statement, the axioms, the statement review and the solution PDF.

Built on

  • Lean v4.35.0
  • Mathlib
  • Stacks Project
  • Lean REPL
  • LaTeX
How it works

The model proposes.
Lean decides.

Every claim the model makes is checked by Lean, and the result shows exactly what was checked.

  1. 01

    Describe it.

    A problem to solve, a statement to prove or a Lean theorem that ends in sorry, with papers or notes attached.

  2. 02

    Prove it.

    The model plans the work and writes the proof in Lean, one checked draft at a time.

  3. 03

    Check it.

    Lean’s verdict states whether the proof compiles with no error and no sorry, and which axioms it uses.

  4. 04

    Keep it.

    The proof, the notes and the full log stay with the run, with a solution PDF once Lean accepts.

Start a run

Start in
plain words.

Describe a problem, a statement or a Lean theorem, and attach papers, notes or images.

Watch the demo
The start page, with a task typed in the composer and ready to start.The start page, with a task typed in the composer and ready to start.
Inside a run

See exactly
what was checked.

The verdict, the proof, its structure and the solution, side by side.

Proved: no error, no sorry and only standard axioms. The statement review is a model’s judgment, not a check.

Lean4Proof — Lean verdictProved
A finished run of Euclid’s theorem: the Lean verdict Proved, the checked statement, the axioms, the statement review and the solution PDF.A finished run of Euclid’s theorem: the Lean verdict Proved, the checked statement, the axioms, the statement review and the solution PDF.
After the verdict

Ask. Edit.
Explore.

Every run stays open for questions, changes and a closer look.

Edit and check

Edit. Check. Repeat.

Change Proof.lean in the app and check it with Lean in one click.

Proof.leanLean 4
theorem imo_1964_p1_b (n : ℕ) : ¬ 7 ∣ 2 ^ n + 1 := by  have h := two_pow_mod_seven n  have hr : n % 3 < 3 := Nat.mod_lt n (by norm_num)  generalize 2 ^ n = m at h ⊢  rw [Nat.dvd_iff_mod_eq_zero]  interval_cases hn : n % 3 <;> norm_num at h <;> omega
No errorsNo sorryStandard axioms only
Follow-up questions

Ask a follow-up.

Every message continues the same session, with its full history.

Comments

Comment on any line.

Select lines to ask a question or request a change.

Proof Graph

See how it fits together.

Every lemma and every use, from the first step to the main theorem.

Your API key

Your model. Your key.

Claude or any OpenAI-compatible model, billed to your own account.

Three ways to run

Mac, browser or terminal.

A macOS app for Apple silicon, a web interface and a command-line tool.

macOS appBrowserTerminal
Your data

Local by design.

Lean4Proof runs on your computer, sends your work only to the model provider you choose and collects no telemetry.

  • Local records.Each run keeps its files, a journal of every check and a report on your computer.
  • A contained agent.No shell and no web access. It writes only the files of its own run.
  • A sandbox for code.Lean and Python run in a sandbox without network access.
  • A local server.Connections from your computer only, and every request needs its token.
Lean4Proof for Mac

What would you like
to prove?

Coming soon for Mac. See a full run in the demo.

Watch the demo
Verified by Lean 4Runs on your computerBring your own API key