Contents
This page is drawn by its script, and this viewer has not run it. Open the file in a web browser.
This page is drawn by its script, and this viewer has not run it. Open the file in a web browser.
Statement.leanlean/SpectreKnot/Statement.lean states Theorems A and B in Lean, with every definition they depend on. The proofs are in other files, and Lean's kernel has checked them against exactly these statements. So whether the right thing has been proved comes down to reading this one file: do its definitions say what the paper means?
The file is shown below in full, piece by piece, with a plain reading of each piece beside it. Click any coloured word in the code for its meaning. New to Lean? Start with Lean for this file; Where to start then suggests a reading order. Notes: ✓ As intended checked against the paper, ! Be aware a subtlety, ◆ Outside Lean something Lean takes as given. Tick a piece once you agree with it; ticks stay in this browser.
Generated by an AI system (Claude) at Justin Roughley's instruction, 13 Oct 2026. It explains the file; it does not replace it. Where this page and the file differ, the file is what Lean checks. The example outputs were produced by running Lean 4.34.1 on the file.