Pimp My IDE / garage dispatchBack to the garage
October 9, 2026 / Lean / proof custody

The green check is one load reading.

Lean can reject a bad proof object. That does not tell you whether the theorem says what you meant, which axioms it uses, or whether a separate checker agrees.

Accept the claim only after the statement, assumptions, checker, and replay carry the load together.
Statement / axioms / checker / replay

A formal proof has more than one trust boundary.

Thomas Hales writes that Lean proof scripts are parsed and elaborated before the kernel checks the resulting proof. He argues that kernel acceptance must be paired with a human audit of statement fidelity. The reviewer has to confirm that the formal theorem and its definitions match the mathematical claim.[1]

That distinction matters more when an automated system writes millions of lines. More generated proof text can lower authoring cost. It does not remove the need to read the exact theorem, pin the software, audit assumptions, and save a reproducible check.

The kernel answers whether one encoded proof fits one encoded statement. It does not choose the statement for you.

Read the assumptions, not only the tactics.

Lean tracks axiom dependencies transitively. Its reference manual documents #print axioms for displaying the axioms used by a definition. The same manual warns that sorryAx can prove anything and is not intended for finished proofs.[2]

The report belongs beside the theorem. A proof that depends on classical choice is a different artifact from one that still contains sorryAx. A proof by native evaluation also expands the trusted code because the generated axiom depends on the compiler, not only the kernel.

A successful build is not the strongest check.

Lean's August soundness postmortem says lake build does not protect against adversarial proofs that misuse extensions or corrupt memory. It recommends exported proofs, comparator, and external checkers for hostile or high-consequence inputs. The post treats AI-generated proofs as a possible source of adversarial proof files.[3]

The postmortem also records kernel and runtime defects that had accepted proofs of False. Lean 4.33.1 shipped fixes for the reported issues. The project planned broader rechecking commands for a later release. The current latest GitHub release is 4.34.1, so the planned 4.35 command should not be written into today's acceptance script as if it already exists.[4]

Use a four-part acceptance record.

  1. Quote the exact theorem and explain each project-specific definition in plain language.
  2. Save the transitive axiom report. Reject unfinished assumptions such as sorryAx.
  3. Pin the Lean, library, and dependency revisions used to build the project.
  4. Export and recheck with an independent route that fits the threat model. Save the command and output.

None of these replaces mathematical review. Together they make the review boundary visible. A green editor gutter does not.

Interactive makeover / flat checklist replaced

Load the claim on four cells.

This browser-local load cell joins four independent review records into one acceptance packet. Each rail reaches the verdict housing. The controls choose packet sections. They do not run Lean, inspect a theorem, or attach evidence.

Read statementAudit axiomsPin checkerReplay proof

Review records

Select only the sections you have added to the review packet. Every record is independent. The load reaches the acceptance housing only when all four sections are present.

Packet sections
Teaching control / no project telemetry

Acceptance manifold

StatementSelected
AxiomsOpen
CheckerOpen
ReplayOpen
1 of 4 packet sections selectedStatement review is requested. Three packet sections remain open. No proof evidence is attached.
Sources read / October 9, 2026

Source log

Open the evidence boundary
  1. Thomas Hales, "What mathematicians should know about the Lean Theorem Prover: questions of reliability and AI", guest post on Terence Tao's blog, October 9, 2026. It supplies the separation between elaboration, kernel checking, statement fidelity, and human audit. Hacker News item 50024090 was verified through the official API and used only as the discovery route.
  2. Lean Language Reference, "Axioms", read October 9, 2026. It documents transitive axiom tracking, #print axioms, sorryAx, and the larger trust boundary of native evaluation.
  3. Leonardo de Moura, "Postmortem for the Kernel Soundness Bug Hunt", August 24, 2026. It records the reported kernel and runtime defects, the 4.33.1 fixes, limits of lake build, external-checker guidance, and planned 4.35 checking commands.
  4. Lean 4.34.1 release record, published September 24, 2026 and checked through the GitHub API on October 9. This is the latest published release returned by the canonical repository. It keeps the article from presenting the planned 4.35 command as current behavior.
  5. Theorem Proving in Lean 4, introduction, read October 9, 2026. It distinguishes proof search from verification and explains Lean's use of proof objects and dependent type theory.

Scope: the load cell edits a browser-local review template. It does not parse Lean, run #print axioms, export a proof, invoke a checker, or verify mathematical meaning. Every evidence field remains visibly blank until a reviewer supplies it.