The Spectre Knot the proofPictures and ideas →
Draft proof, not peer reviewed. What has been checked

The Spectre Knot theorems and their proof

The block N2 of the nest tiling, its ribbons drawn in fine lines
N2 of the nest, with N1 dashed and the first tile shaded: no strand closes, and the first tile’s pieces lie on just the two tinted arcs.

A reader’s guide to the proof that the Spectre Knot has no closed loop in any spectre tiling whose supertiles fill the plane, and is one endless strand in the nest tiling, grown outwards from a single tile, each block sitting in the same place (child number 1) inside the next. These pages show what is proved, by which route, and how the results of the paper hang together; every result has a page with its statement and proof from the paper, what it cites, what cites it, and the Lean that formalises it. The paper has not been peer reviewed.

Read the paper

The whole proof as the paper sets it out: the PDF, or here, result by result, each with its statement and proof.

the PDF of 22 October 2026, 28 pages

Follow the argument

Ten steps, one for each section of the paper, each with its results and a small graph of how they depend on each other.

See the structure

Every result in one graph: what rests on what, and which are argued, computed, cited or also in Lean.

Read the Lean

The statement file line by line, beside a plain reading of each piece; then every file of the formalisation, in full.

Statement.lean

Get the code

The programs the computations use, with their logs, and the Lean: where they are, and how to build and run them.

GitHub · the zip

What is proved

Theorem A · the Daedalus Theorem argued Lean, in part

In every homochiral tiling of the plane by $\Tile$ whose supertile hierarchy covers the plane, with every tile carrying the decoration of Figure 1 (Definition 3.1), there is no closed strand: every strand is a two-way infinite path of ribbon pieces.

Theorem B · the Ariadne Theorem argued Lean, in part

In the nest tiling $\N$, with every tile carrying the decoration of Figure 1 (Definition 3.1), all the ribbon pieces of all the tiles form a single strand. It is a two-way infinite path that passes through every tile. More precisely, for every $b\ge 1$, all the pieces of the block $N_b$ lie on a single arc of $N_{b+3}$ if $b$ is even, and of $N_{b+4}$ if $b$ is odd.

In Lean 4, the two main theorems. Their claims, TheoremA_strand and TheoremB_strand, are written out in the statement file in a combinatorial form, with patches and tilings described by which edges are glued:

theorem theoremA_strand : TheoremA_strand
theorem theoremB_strand : TheoremB_strand

The build, lean/build.sh, runs #print axioms on the main theorems (lean/Axioms.lean) and fails unless the answer is among Lean’s standard three, propext, Classical.choice and Quot.sound: no sorryAx, no Lean.ofReduceBool. It also fails if a main theorem no longer proves exactly its claim in the statement file, if the statement file or a file it imports has changed since its SHA-256 was recorded, or if leanchecker, replaying every declaration through the kernel, finds a problem. The public repository’s checks also run comparator, the Lean developers’ tool for judging whether proofs prove exactly the statements of a trusted file: it confirms that the main theorems prove exactly the claims of the statement file (lean/tools/comparator.sh).

That actual spectre tilings are glued as the formal statements assume is argued in the paper, not formalised: what the Lean does not cover.

The proofs and their Lean were generated by an AI system at Justin Roughley’s instruction, and the paper has not been peer reviewed: how this was made, and what has been checked.

Theorem A’s page → Theorem B’s page →

The top of the proof. Premises above conclusions: an arrow runs from a result to one whose proof cites it, possibly through results not drawn here. Click any card; the whole graph.

The route

The proof climbs the supertile hierarchy. First it shows that every supertile, of every kind and level, looks the same from outside; then it follows the ribbons up the nest. Step 1 sets out the two theorems and the method; steps 2–7 prove the Daedalus Theorem; steps 8 and 9 add the Ariadne Theorem; step 10 says what is covered. The ten steps are those of the public site’s Prove page, which explains each with pictures, and step n follows section n of the paper.

The route: ten steps, each with its results →

The numbers

36numbered results, definitions and remarks in the paper
28results in the graph
47citations by number between them
12longest chain of citations up to a main theorem
4greatest depth: shortest chain from a result up to a main theorem
3finite checks done by program
22results also checked in Lean, fully or in part
855Lean declarations, each with its own page
12,146lines of Lean, not counting the generated data files

What the Lean checks, and what it does not

What it checks

The Lean formalisation proves the results marked Lean about patches described by which edges are glued: every supertile has the signature (Theorem 7.6); in the union of any chain of supertiles in which every edge is eventually glued, every strand is two-way infinite (Theorem A), and the nest is such a chain; the nest tiling, as the union of its blocks, is one two-way infinite strand (Theorem B), with the bounds of Theorem 9.1, which are exact; and every vertex of a tile of a block of the nest is surrounded by the block two levels up (Lemma 8.3, at the vertices of tiles). Its kernel also re-runs the finite computations these use (Computation 7.5 on the level-1 supertiles that exact.py computes, taken as input).

Its statement file, lean/SpectreKnot/Statement.lean, with the three files it imports, holds every definition the main theorems use, so whether the right thing has been proved comes down to reading them: the statement file, line by line.

What it does not cover

From lean/README.md.

  • The link with tilings of the plane: assumption (M), written out at the top of Statement.lean in three parts. The formal statements are about patches and tilings described by their gluing; each part is argued in the paper and none is formalised.
    • (M1) Supertiles. That the supertiles of an actual tiling are glued like super m K. It rests on the spectre paper and on the paper's §2 and §7.1: Thm 2.1 (the hierarchy, from the spectre paper), Prop 2.4 (the composition pattern holds at every level), Remark 2.5 (its cross-checks on actual supertiles, evidence not used in the proof), Lemma 2.6 (rigidity), Def 2.2 (own orientation, built into compose) and step (ii) of §7.1 (two children meet only in the sides they share). In Lean, Tables 1–4 are simply data.
    • (M2) Theorem A for tilings. TheoremA_strand is about the union of a chain of supertiles that covers, that is, in which every edge is eventually glued. That a tiling whose hierarchy covers the plane is such a union is the first step of the proof in §7.4, about points of the plane.
    • (M3) Theorem B for the nest tiling of the plane. TheoremB_strand is about nestTiling, the union of the blocks super b .Delta. That this is the nest tiling of the paper, and that it covers the plane, is Prop 8.2 and Prop 8.4, which are geometric. Lemma 8.3(a), which Prop 8.4 uses, is formalised for the vertices of tiles (Grandparent); the step from those to points of the plane is part of (M3).
  • Lemma 4.1 for a general patch. Only patches with the signature are given a box (Patch.HasSig.box); following a ribbon (Follow) plays the role of π_P.
  • The corner A at level 1. The paper defines the corner A of a level-1 supertile as v₀ of the first tile of its Mystic. The Lean takes its position from the data (vertex 0, or for Σ the point d₁ along side 5), and does not pick out the Mystic among the tiles of the level-1 supertiles; above level 1, A is the Γ child's (cornerA_succ).
  • The second routes of Appendix A. The skeletons, and the label states with certified inequalities, are not formalised.
  • Exact counts. The last two rows of Table 5 are proved (TheoremB_exact); the rows for each b (such as 10, 37, 146, 613 arcs one level up) are computed by the tests for small b, not proved for every b.
  • The drawing, and §10. The drawing itself; the three strands along another chain (the tests compute its first counts); and faults.
  • Data are input. Tables 1–4 come from combin.js (the composition pattern computed from the geometry, and checked against the spectre paper's figures by the paper's scripts); the level-1 supertiles come from exact.py. The Lean checks the level-1 supertiles' signature itself (good_one), but not that they are the spectre paper's clusters.

Marks