MachineChecked

Read a mathematical paper beside its Lean formalisation.

Select a statement to inspect its Lean counterpart, proof results and correspondence reviews. MachineChecked runs locally in your Lean project and saves the links you choose.

Try the demo · Browse papers · Setup guide

Open your paper

From your Lean project's directory:

lake build
uvx machinechecked view

MachineChecked finds the paper and opens the reader. You can also name a LaTeX file, PDF or URL:

uvx machinechecked view paper/main.tex

Requires Python 3.11+, your project's Lean toolchain, and TeX Live for LaTeX or Poppler for PDFs. The web reader is included. For a persistent command, run uv tool install machinechecked; then use machinechecked directly.

Select a claim from the contents or paper margin. Expand comparison shows the paper, complete readable statement and exact Lean together. Follow existing \lean{...} tags, confirm a suggestion, or choose a declaration. The reader saves your choices in machinechecked.links.json. Projects with a formalization.yaml supply their paper sources and declared links automatically.

Read the evidence

A Lean proof establishes a formal proposition. A correspondence review compares that proposition and its definitions with the paper. Source checks identify the audited text; independent kernel replay checks the proof again. The reader shows each result and its provenance in Audit details.

The optional Review view guides you through three steps:

1. Read the paper and record your interpretation.
2. Compare the Lean statement's assumptions and conclusion; record a verdict.
3. Read the author's review, save your report in the browser, and export it.

The maintainer evaluates reports and promotes reviews into the project's acceptance records. Review guide →

Share the reader

uvx machinechecked build                 # .machinechecked/MachineChecked.html
uvx machinechecked build --site public/  # a static site with audit.json
uvx machinechecked check                 # check linked declarations for automation

The HTML file opens directly in a browser. It includes the paper, Lean statements and audit data; review those contents before publishing. Host the site directory on GitHub Pages or another static host. Published audits carry their author's name, project commit and paper revision.

Copy link shares a claim. Report issue opens a draft in the audit's GitHub repository, with the claim identifier, declarations and commits filled in. Set that repository with --issues owner/repo.

With a coding agent

machinechecked check --json prints structured results for scripts and agents. The MachineChecked skill covers commands, status codes and evidence. Agent guide →

Full assessment

Projects with locked specifications, a claim inventory and review records can configure machinechecked.toml. Full assessment adds exact-type checks, definition-dependent reviews, witnesses, refutations and independent kernel replay. Configuration guide →

Documentation

• Get started — install, open, link, share and troubleshoot
• Reviewing — record mathematical judgements
• Full assessment — configuration and acceptance
• Evidence policy — what each check establishes
• Data model · Publication policy · Threat model
• Development · Plan

Apache-2.0 licensed.