A Lean build says the Lean theorems are proved. It does not say they are the paper’s theorems. MachineChecked opens a paper beside its formalisation and shows, claim by claim, which Lean declaration it corresponds to, whether Lean proves it, and whether anyone has checked that the two say the same thing.
In the paper
Proposition 2.3. Every natural number is strictly greater than its predecessor n − 1.
From the demo’s synthetic paper. With truncated subtraction, 0 − 1 = 0, so the claim fails at n = 0.
What was established
It finds the paper, reads every numbered statement from the compiled LaTeX, and indexes the project’s built declarations. Nothing to configure.
\lean{…} tags and suggestions become links you confirm in the reader. Each claim then says exactly what Lean establishes: proved, incomplete, extra axioms, or not found.
Write the reader as one HTML file, or publish it. Anyone reading it can raise an issue on a claim, with the claim, the Lean declaration and the commits filled in.
Inside a built Lean project (lake build), with Python 3.11 or later and TeX Live for a LaTeX paper:
uvx --from git+https://github.com/cgarryZA/ProofLens machinechecked view
machinechecked build writes the reader as one file to share; machinechecked check fails CI when a linked declaration is missing or unproved. Reviews, locked statements and an acceptance status per claim are there for projects that want a full audit. Read the guide.