The interactive map needs JavaScript. Every object it shows is in the lists in the panel, and the complete graph is published as graph.json.
Proof tested against separate statementStated in Lean; comparison not recordedStated in Lean with extra assumptionsNo Lean statement yetWritten proofShort paper, inner rowsLong paper, outer rowsExpository paper, beside its problem
What the map shows
Result
A theorem, lemma or proposition printed in one of the papers. Each dot in the outer ring is one result.
Short paper and long paper
Each problem has two papers. The short paper states the main results and grounds them in the literature; the long paper keeps the whole investigation, including the routes that failed. In each problem’s band the short paper’s results fill the inner rows, on a brass wash, and the long paper’s the outer rows, on a violet one.
Expository paper
A paper for a reader new to a problem. It explains one result of the problem’s short paper with worked examples and proves it in full, so it adds no results of its own; its mark sits on the orbit beside the problem, in verdigris.
Claim
A headline statement in a problem’s record, such as a theorem about the problem or a reduction of it to a simpler question. A proved claim has the proof or finite verification described in its record. Unconditional progress is a proved partial result. A conditional reduction proves that a conclusion follows from listed assumptions that remain unproved. An open claim has no proof recorded. The claims sit in the ring just outside the problems.
Lean
Software that verifies a formal proof against a precisely written theorem statement and its assumptions. A result is exact in Lean when a Lean theorem states what the paper states, and under named inputs when the Lean theorem also assumes an additional named hypothesis. The proof does not establish that hypothesis.
Comparator
A Lean tool that checks a proof against a separately written statement of the theorem, so a proof of a weaker or different statement fails. A replay is a recorded run of that test on the listed proofs and statements.
Palomar
An external registry for results with computer-verified proofs. Selecting it shows the recorded preparation or registration status and links to the dated records.
Plectis