lean-xray
Lean is a program that checks mathematical proofs. lean-xray shows what those proofs rely on and flags unfinished steps.
Source not currently publicRecorded research exhibit
Follow one assumption
Recorded demonstration · Deep audit
Lean accepted the proofs using the example’s stated assumptions. The audit verdict was REJECT.
The first result relies on the deliberately false assumption that 2 + 2 = 5. Open Demo.ordinary below to compare it with a proof of 2 + 2 = 4.
Demo.conclusion
Demo.conclusionDemo.starting_point
The arrow means the proof relies on the assumption, either directly or through another proof.
Recorded axiom dependencies: Demo.starting_point.
The source scan recorded no finding for this statement. The assumptions above come from a separate check.
Demo.intermediate
Demo.intermediateDemo.starting_point
Recorded axiom dependencies: Demo.starting_point.
The source scan recorded no finding for this statement. The assumptions above come from a separate check.
Demo.starting_point
Demo.starting_point
Recorded axiom dependencies: Demo.starting_point.
A004: project-local axiom starting_point. Classification is a source heuristic.
Demo.ordinary
Demo.ordinary
Recorded axiom dependencies: none in this checked declaration.
The source scan recorded no finding for this statement. The assumptions above come from a separate check.
Inspect fixture source Demo.lean
namespace Demo
axiom starting_point : 2 + 2 = 5
theorem intermediate : 2 + 2 = 5 := starting_point
theorem conclusion : 2 + 2 = 5 := intermediate
theorem ordinary : 2 + 2 = 4 := rfl
end Demo
Audit details and grades
- Absolute grade
- D1 Counts what the audit found regardless of which assumptions a reviewer accepts.
- Bounded grade
- D1 Can set aside certain axioms if a reviewer explicitly accepts them.
- Recorded check
- Build passed; axiom closure recorded
D1 flags findings such as an unfinished proof in the source or an axiom the project added.
The policy verdict records the decision under the reviewer’s rules.
Path basis: Emitted axiom membership; direct or indirect use, not proof-term causality.
leanprover/lean4:v4.31.0. Earlier check: Fast source scan; it did not establish this dependency.
lean-xray 1.9.0 · 2026-09-22T04:01:02.373303+00:00
Tool revision 7592bd633327e50ab01216bbd1f2fb83407c8913
This deliberately false assumption belongs to a demonstration, not a production project or Mathlib report. Lean built the fixture relative to its stated axiom; that does not make the assumption true. The deep report establishes axiom membership, not exact proof-term causality or an independent kernel replay.
A successful build can still deserve rejection
Lean checks whether a proof follows from the rules and assumptions it was given. When you review the result, you may still want to know which assumptions the proof used, whether any steps were left unfinished, and whether the statement being proved changed since the last review. lean-xray gathers evidence for those questions. The Lean community’s proof review checklist explains why they matter.
In the example above, the line marked axiom tells Lean to take 2 + 2 = 5 as a given. Lean accepts proofs that follow from that starting point. The audit shows which proofs relied on it.
The fast source scan found the axiom, but did not establish the downstream dependency. A subsequent deep audit built this small fixture with Lean 4.31.0 and emitted per-declaration axiom membership. The ordinary two-plus-two-equals-four theorem had no axiom dependencies in that report.
What the trace establishes
The displayed relationship means a checked declaration uses the axiom directly or indirectly. Other declarations carrying the same axiom are not necessarily steps along its proof path. The figure therefore does not draw them as intermediate causes.
This is a newly authored demonstration fixture, not a report about Mathlib or another project. No independent kernel replay or performance benchmark is claimed. The selected result excludes the raw local manifest, machine paths, and unrelated findings.
Ordinary Lean axioms such as propositional extensionality, classical choice, and quotient soundness are not automatically defects. The false arithmetic axiom here is deliberately different. Dependency findings, checker coverage, correspondence with the intended statement, and mathematical interpretation remain separate review tasks.
Project details
Added · Updated