Will Cook’s home page: all projects and videos
Proof Reader displays a research paper beside its proof in Lean, a language for writing mathematical statements and proofs that a computer can check. Click a linked statement in the paper to open the authors' corresponding Lean code. You can also explore a diagram of the proof steps and the connections between them.
Read a paper in it: Contextual Embeddings by Frohlich, Foster, Kavvos and Wang (PLDI 2026), shown with the authors' Lean under CC BY 4.0. The links and comparisons between the paper and the Lean were made with AI and have not been reviewed by the authors.
For a specific example, open a paragraph and its five linked lines of Lean, linked to Lean lines 217 to 221.
On a desktop, the paper is on the left and the proof diagram is on the right. As you scroll, the diagram highlights the step linked to the passage you are reading. Click a statement or diagram card to see its Lean code. Use Back to return to the diagram without losing your place, or the Graph / Lean toggle to choose what stays beside the paper.
Citations and figures open beneath the paragraph that mentions them. Each linked statement has its own address, so you can send someone directly to it. The contents also include an index of named Lean definitions and theorems (called declarations), with the assumptions each proof uses (axioms).
The site adds no explanation of the mathematics. A program checks the reading copy against text extracted from the PDF, and the original PDF is one click away. The graph's edges and the axiom lists come from Lean's own report on the authors' files, read from the compiled project. The only added words are a short plain title for each declaration, short notes where the paper and the Lean differ, and a comparison of each stated result with its Lean statement, each linked to the sentence it is about. These links, titles, notes and comparisons were made with AI and have not been reviewed by the authors. Where a comparison cites a Lean proof written for the page, the proof is shown with it, and Lean accepted it against the authors' code.
Use Python 3.11 or later, Node 20.19 or later, and Poppler
(brew install poppler on macOS; sudo apt-get install poppler-utils on Ubuntu).
From a fresh clone:
git clone https://github.com/wcook04/proof-reader.git
cd proof-reader
cd web
npm ci
cd ..
python3 tools/paper.py build
cd web
npm run devOpen the address it prints and choose Contextual Embeddings. The paper build creates
the data the site needs; it uses the checked-in Lean extraction, so running the existing
paper does not require Lean. After changing a paper's files, run python3 tools/paper.py build
again from the repository root.
From web/, npm run build writes a static site to web/dist.
npm run preview serves that build locally. If you set VITE_BASE_PATH for
the build, use the same setting for the preview. For example, a build made with
VITE_BASE_PATH=/proof-reader/ npm run build needs
VITE_BASE_PATH=/proof-reader/ npm run preview.
To test the reading controls in a real browser, build the site and run the
browser test script. It needs Playwright for Python, and takes --browser firefox or webkit as well:
cd web && VITE_BASE_PATH=/proof-reader/ npm run build && cd ..
python3 tests/journey.py --shots /tmp/journeytests/speed.py measures a paper's first screen on a home connection.
tools/capture_images.py retakes the social card and the picture above from a running site.
To add a paper, create a folder containing the original PDF and Lean project, a reading copy of the text, and links between passages and Lean statements. The build command turns those files into pages for the website.
papers/<slug>/
paper.pdf the authors' PDF, unchanged
paper.md a reading copy of the paper, checked against text from the PDF
paper.toml title, authors, licences and the Lean modules to read
lean/ the authors' Lean project, unchanged
links.json which passage goes with which declaration, plain titles, notes and comparisons
checks/ optional Lean files of ours that test a statement against the authors' Lean
generated/ what Lean reports about the project and the checks
The add-paper guide gives the full procedure for a person or an AI assistant. The commands are:
python3 tools/paper.py new my-paper # then add the PDF, Lean and paper.toml
python3 tools/paper.py extract my-paper # build the Lean, list its declarations, compile checks/
python3 tools/transcribe.py my-paper # draft paper.md from the PDF's structure
# define a result under claims in links.json, with its passage and Lean declaration
python3 tools/paper.py check my-paper # compare the text and check the links
python3 tools/paper.py build # write the data the site readsextract needs elan, the Lean installer,
and uses the Lean version specified by the paper's authors. check and build need Python 3.11 and Poppler, and, for
a paper with a paper.md, Node with npm ci run in web/. transcribe.py also
needs pypdf. The authors' code runs on your machine, so read a project you do not
trust before extracting it.
The command compares the reading copy with text extracted from the PDF. It skips the top 7.5% and bottom 5.5% of each page, repeated headers and footers, bullet marks, and words inside figure crops. The figures themselves are copied from the PDF.
It treats some typographic differences as equivalent, such as ligatures and line-break hyphens, and allows text blocks to move. These allowances can also let changes in word or character order pass. The check helps find transcription errors; a pass does not certify an exact copy. Review the reading copy alongside the original PDF.
The command also confirms that every quotation appears exactly once, that exact Lean lines lie
inside their declaration and that every Lean name exists. No program confirms that a sentence is
about the code it is linked to: a person has to read both. Names printed in the paper are linked
by matching the name alone, so STLC in the paper's Haskell opens the Lean STLC. Lean reports
what a proof depends on, and does not report whether a Lean statement means what the paper says.
So every result the paper states, and every axiom of the authors, carries a comparison: the Lean
says the same as the paper, more, less, or something different. check stops if one is missing.
A comparison is AI judgement. Where it cites a check, the check is a Lean file of ours under
papers/<slug>/checks/, compiled by extract against the authors' Lean, with the axioms Lean
reports for it. check stops if a check file has changed since extract compiled it. Each page
says that the links, notes and comparisons have not been reviewed by the authors, until an author
has reviewed them.
Authored paper files and the checked-in Lean extraction live under papers/.
tools/paper.py build turns them into web/public/papers/. The website build
command then packages them with the application in web/dist/. Both output directories are ignored by Git:
change their sources and rebuild them.
| Source | What it holds |
|---|---|
| papers/ | One folder for each paper |
| skills/add-paper/ | How to fill in a new paper |
| tools/paper.py | Extract the Lean, compare with the PDF and build the data |
| tools/transcribe.py | Draft a paper's reading text from its PDF |
| tools/reading.py | Compare the reading copy with the PDF and mark its linked statements |
| render-paper.mjs | Typeset paper.md with Markdown and KaTeX |
| extract.lean.template | The Lean program that lists a project's declarations |
| web/ | The website |
| web/src/map/ | The map, copied from lean-exposition |
| history.ts | Saved reading position and open statements for the Back button |
| web/src/lean/ | Code for displaying and colouring Lean source |
| web/src/proof/ | The proof diagram and Lean panel beside the paper |
| check-source.mjs | Find source files that the application and tools do not use; run with npm run check:source in web/ |
| tests/ | Python unit tests and the browser journey |
| Pages workflow | Check every paper, build the site and publish to GitHub Pages |
Lean Exposition contains writing guides and tools for explaining a Lean proof in three papers with different levels of detail. Its reading website presents those draft explanations beside the graph; this video walks through that site. Proof Reader's reading copy keeps the original paper's wording.
Code is Apache-2.0; see LICENSE and NOTICE. Each paper and Lean
project keeps its own licence and credit, named in its paper.toml and on its page.
Proof Reader is one of Will Cook's sites. Find the other websites and code on Will's home page, and the project videos.