← Work

lean-xray

In Progress

Inspect the assumptions behind a Lean declaration, and what the audit actually checked.

Demonstration fixture · Deep audit

Follow one assumption

Open a declaration to inspect its relationship to the demonstration’s assumption. The source and the scope of the check are available below.

Absolute grade
D1
Bounded grade
D1
Policy verdict
REJECT
Recorded check
Build passed; axiom closure recorded
Demo.conclusion theorem · line 4
  1. Demo.conclusion
  2. Demo.starting_point

Recorded axiom dependencies: Demo.starting_point.

No source finding is attached to this declaration. The recorded axiom membership above is a separate check.

Demo.intermediate theorem · line 3
  1. Demo.intermediate
  2. Demo.starting_point

Recorded axiom dependencies: Demo.starting_point.

No source finding is attached to this declaration. The recorded axiom membership above is a separate check.

Demo.starting_point axiom · line 2
  1. Demo.starting_point

Recorded axiom dependencies: Demo.starting_point.

A004: project-local axiom starting_point. Classification is a source heuristic.

Demo.ordinary theorem · line 5
  1. Demo.ordinary

Recorded axiom dependencies: none in this checked declaration.

No source finding is attached to this declaration. The recorded axiom membership above is a separate check.

Path basis: Emitted axiom membership; direct or indirect use, not proof-term causality.

Inspect 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

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.

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

A successful build can still deserve rejection

The demonstration deliberately introduces the false assumption that two plus two equals five. Two theorems refer back to it. Lean can check those theorems relative to the assumption; compilation does not establish that the assumption is true.

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.

Absolute grade, bounded grade, and policy verdict answer different questions. In this run both grades are D1 and the verdict is REJECT. A passing build does not erase the finding.

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.

leanproof-trust

Added