Made with AI: an experiment
The Spectre Knot is an experiment in using AI for mathematical exploration. Justin Roughley came up with the original idea of looking for a mono‑stranded aperiodic knot, and then used AI to search for it. From then on an AI system (Claude, by Anthropic) did the detailed work at every stage, always at his instruction: it generated the programs, the proofs of the two theorems, a formal version of the proof that the Lean proof assistant checks, the paper, this website and the handout. He set the direction, made the choices, questioned the work and had it corrected. Justin Roughley is the author, and is responsible for the work, including its correctness; the AI is not an author.
The status of the proof
The proofs and the Lean were generated by the AI at Justin Roughley’s instruction. Lean checks the combinatorial heart of the proof; the step linking it to actual tilings of the plane (how real supertiles fit together) is argued in words. Justin Roughley has read parts of the paper and spot-checked pictures and counts; most of the proof has not been reviewed by a human, and no professional mathematician has reviewed it. No human has checked that the Lean’s statements say what the theorems say. The paper has not been peer reviewed.
AI can turn out a great deal of plausible-looking mathematics very quickly. That is why the proof was also written for Lean, whose checker verifies every step mechanically, and why this page sets out plainly who did what.
Who did what
| What | Justin Roughley | The AI system, at his instruction |
|---|---|---|
| The question | Asked it: is there a one‑strand knot that covers the plane? | – |
| Searching for designs | Asked for the search and steered it | Generated and ran the search programs, which found 34 candidate designs |
| Design 0.1:01 | Chose it, drew its ribbons by hand, and chose the offset of the crossing points along the edges | Generated the tile editor he drew it in |
| The computations, up to 133 million tiles | Asked for them | Generated and ran the programs |
| The proofs of the two theorems | Asked for a proof; directed the work, questioned it and asked for corrections; decides what is claimed | Generated the proofs: the method, the lemmas and the arguments |
| A formal version of the proof’s combinatorial part, for the Lean proof assistant | Asked for it | Generated it; Lean checked every step |
| The paper setting out the proofs | Directed it, and specified that it follow the Leiden Declaration on artificial intelligence and mathematics | Generated the text and the figures |
| Naming the theorems and lemmas (the Daedalus Theorem, the Ariadne Theorem, the Signature Theorem; the Zigzag and Grandparent Lemmas) | Chose the names | Suggested names |
| This website, the handout and the tile | Set the brief, made the decisions and asked for changes | Generated them |
| Checking the proof | Read parts of the paper and spot-checked pictures and counts | Reviewed the argument in several passes; generated the second programs used as checks |
| Credit and responsibility | His alone: he is the author | None: it is a tool, not an author |
No professional mathematician has reviewed the proof. An AI system builds on mathematics that people have published: the work this rests on is credited on About and in the paper, and the paper says that it may use an idea whose source it does not cite.
What has been checked
What has been checked, by Lean, by computer, by the AI and by Justin Roughley, and what has not, is set out on the proof site: What has been checked. On this site, the Prove page marks each step as cited from the spectre paper, computed, or argued in words, with a Lean tag where Lean also checks it, and says exactly which tilings each theorem covers. Every program, including the second or separate ones used as checks, and the Lean, was generated by the same AI system. Every tool used is listed in the paper’s Tool and computational resource disclosure.