Method

Method

Every record is assembled by a scheduled job from a public source. Nothing is entered by hand. Where a source cannot be read, the failure is shown in the footer rather than hidden, and the affected records are left as they were.

Two kinds of node

A statement is a proposition: it is open, or it is settled. A target is a quantity: it has a direction, a history of values and a current record. Much of what artificial intelligence contributes to mathematics is not a settled proposition but a moved number or a better object, and a register holding only propositions cannot record it.

A record is a value together with who reached it and when, so whether a machine currently leads a target is a query rather than an opinion. Where a source publishes only where a construction stands and not what it measures, the standing is recorded and the value left empty rather than invented.

Record standings

below

Did not reach the best known value

matched

Equalled the best known value

record

Best known value

superseded

Held the record, since beaten

unstated

No standing recorded at source

One statement, one record

The register is a graph of mathematical statements. A statement — a problem, a conjecture, a theorem — is a node, and its formalisations, cited proofs, recompilations, prizes, tags and every claim made about it attach to that node exactly once.

Identity is source-anchored. A statement's canonical id names the collection that owns it, such as erdos:707 or kourovka:12.34, and every other locator that denotes the same statement — a Lean path, a problem page — is recorded as an alias. Two records are merged only when a locator says they are the same. They are never merged because they look alike, since two faithful formalisations of one problem can differ and two different problems can read almost identically.

Relations

derives-from

whose proof imports the proof of

part-of

is one component of

references

cites, in its source text

variant-of

is a modified form of

Edges are only recorded where a source supplies them: a citation in a Lean file that resolves to another statement held here becomes an edge, and nothing is inferred from similarity. The graph is therefore sparse, which is the honest condition rather than a shortcoming.

Three grades, not one verdict

A claim is a point in three dimensions. Autonomy records how much of the mathematics the machine did alone. Evidence records how strongly the result is attested. Fidelity records whether the formal statement that was checked says what the claim says. They are independent: an autonomous result can be poorly evidenced, a heavily supervised one can be machine-checked, and a machine-checked proof can prove a statement nobody has compared with the claim.

Autonomy

A?

Not established. Declared by whoever submitted the work and not verifiable from the record.

A3

Autonomous. The system produced the result without significant human mathematical involvement.

A2

Directed. The system produced the result while building on literature or framing supplied to it.

A1

Collaborative. A human and a system worked the problem together, or the system played a supporting role.

A0

Human. No machine contribution to the mathematics.

Autonomy is derived from the section placement used by the Erdős problems AI wiki, so the register remains interoperable with the record it continues. Sections 1(a) and 1(b) map to A3, 1(c) to A2, 1(d) and all secondary contributions to A1.

Evidence

V3

Machine-checked. The artifact was rebuilt at a pinned commit by someone other than its authors — qed.bot, or a registry that publishes the check — and it holds: a proof that elaborates on the standard axioms alone, or an object that meets the problem's own constraints.

V2

Artifact reported. A proof or a constructed object is published, but nobody independent of its authors has rebuilt it.

V1

Informal. A public write-up exists and has had community scrutiny.

V0

Claimed. No public artifact, or the claim is marked unverified at source.

V3 rests on a rebuild, never on a report. qed.bot rebuilds proofs and objects itself, and cites Palomar's registration where Palomar has rebuilt a project the register already cites for the result. Every check names who ran it. A registration attached only because a project names the problem is shown, but it is not counted, since a formalisation titled after a problem may prove only part of it.

Outcome

candidate

Unverified candidate

full

Full resolution

incorrect

Incorrect work

partial

Partial progress

unstated

No outcome recorded at source

Fidelity

F3

Anchored. The proof is checked for exact statement identity against a statement written independently of it, held here from a separate statement corpus.

F2

Declared. The authors record how the formal statement corresponds to the claim — a comparator challenge, an alignment table or written divergences — or a statement corpus cites the proof against its own statement.

F1

Unaudited. A formal artifact exists, but nothing records that its statement says what the claim says.

F0

None. No formal statement is attached to the result.

Lean settles whether a proof is valid. It cannot settle whether the statement proved is the one that was claimed. The strongest answer available is a proof checked for exact statement identity against a statement somebody else wrote, and a project can declare that it has done so: its formalization.yaml names a statement from a separate corpus among its related formalisations, and its Comparator configuration checks the proof against it. Where that statement is one this register holds, the result is anchored.

Fidelity is computed from what is declared and held, never from reading the mathematics. It is graded per claim, from the declarations of the repositories each claim cites, so one project's gaps are never read as another's. Beside the grade the register records what it does not fold into it: results assumed from the literature rather than proved, declared divergences from the source, unproved goals, further axioms, review by the authors alone, and any contradiction with a rebuild.

Disclosure

D3

Checkable. Every result announced is identified, and each carries a machine-checkable artifact.

D2

Written up. The results are identified and written up, but not all carry a machine-checkable artifact.

D1

Named. The results are identified but not written up.

D0

Withheld. Results are claimed without being identified.

An announcement is graded for how much of what it claims can be inspected. A result that has not been identified cannot be graded for autonomy, evidence or fidelity, so it is counted rather than placed.

Recompilation

A cited proof earns V3 only by being rebuilt. The checker resolves the project's dependencies at the pinned commit, elaborates the cited file, and appends #print axioms for every theorem it declares. A proof passes when the file elaborates and no theorem depends on anything beyond Lean's three standard axioms — propext, Classical.choice and Quot.sound.

A dependency on sorryAx means an unproved goal survived into the final term, and no amount of successful compilation makes that a proof. Any other axiom is reported by name, because introducing one silently assumes exactly what a formal proof is supposed to rule out.

Recompilation verdicts

verified

The file elaborated and every theorem rests on the standard axioms alone.

axioms

The file elaborated, but a theorem depends on something further — typically Lean.ofReduceBool and Lean.trustCompiler, the signature of native_decide.

incomplete

A theorem depends on sorryAx: an unproved goal survived into the final term.

fragment

The file imports modules from its own project, so it is a statement or a fragment rather than a standalone proof.

no deps

The project's dependencies could not be resolved at the pinned commit.

failed

The file did not elaborate against its own declared dependencies.

Comparing registries

Other projects record the same results under their own vocabularies. Their entries are joined to this register on keys a source actually supplies — the Erdős problem an entry names, the file a proof lives in — and never on a resemblance of titles.

A repository or file holding more than one problem is a container rather than an identity, and is dropped from the join. Without that rule a corpus of a thousand statements would merge every problem inside it into a single record, which is the same mistake as merging two statements because their titles look alike.

Positions are placed in coarse buckets so that two scales can be set against each other at all, and each registry's own label is kept beside the bucket. A bucket is a lens rather than a verdict: some of the distance between two positions is a difference of scale, and the raw labels are shown so a reader can tell which.

Kinds of finding

disagreement

Two registries differ on who did the mathematics. Autonomy has no ordering, so this is a difference of judgement and neither side is corrected here.

gap

One registry holds stronger evidence than another. The evidence ladder is ordered, so this is not a contradiction: one of them knows something the other does not.

lead

Somebody else records a proof this register has not rebuilt — a repository worth fetching rather than an opinion.

probe

Every cited repository is asked whether it contains any Lean at all. A machine-checked grade is a claim about an artifact, and that claim is checkable without rebuilding anything.

The formal record

A Lean project can publish a formalization.yaml in the mathlib-initiative schema, declaring what it proves, the axioms its main results rest on, what it assumes from the literature, how the work was produced and who reviewed it. The register reads every one it can locate: from a seed list gathered by GitHub code search, from every project Palomar has registered, and from every repository the register already cites.

A file with that name is not necessarily a live declaration. Projects keep copies of earlier states under review, verification and history directories, and some keep one directory per version of a result. Those copies are set aside before anything is read, and only the newest version stands, so one project is one declaration.

A declaration joins a statement or a record only on a key a source supplies: a statement it names as its anchor, a cited proof that lies inside its project, or an Erdős problem it names outright. A declaration joined to several results is a container and speaks for none of them. Where a repository or directory has moved, the move is recorded with the commit that documents it, so a link written before the move still joins what it always meant.

Palomar rebuilds a project at a pinned commit, confirms with Comparator that the proof proves the recorded statement within its axiom policy, and replays it through Lean's kernel and the independent nanoda kernel. Where Palomar has registered a project this register cites for a result, that registration is the check, attributed to Palomar, rather than a second rebuild. A declaration that a rebuild contradicts — an axiom found that it does not list, an unproved goal where it records none — is published as contradicted.

Checking an object

A construction is not verified by rebuilding an argument but by testing the thing itself against the constraints of the problem it answers. A cap set is checked by confirming that no three of its points are collinear; a matrix multiplication algorithm by confirming that its decomposition reproduces the multiplication tensor exactly.

This is decisive where it applies, and cheap: seconds, against the hour and several gigabytes a Lean proof costs. The checker never reads the claim it is testing, so it cannot be led toward agreeing with it — the measurement is taken first and compared afterwards, and a measurement that disagrees is published as a refutation rather than discarded.

How a check was made

evaluator

qed.bot rebuilt the object and tested it against the problem's own constraints.

lean

qed.bot rebuilt the proof and inspected every theorem's axioms.

palomar

Palomar rebuilt the project at a pinned commit and registered it; the register cites that check rather than repeating it.

Artifact inspection

Formal statements sometimes cite a Lean proof held in another repository. Every cited file is fetched and read for unproved goals, declared axioms, admit and native_decide. A file that cannot be retrieved is recorded as missing rather than quietly dropped.

This is a static read of source text. It cannot establish that a proof is correct, and it does not earn a V3 grade.

What an outcome refers to

Primary contributions concern the statement: a full resolution means the statement was resolved. Supporting contributions — formalisation, literature search, rewriting, computation — carry outcomes describing that task instead, so a full outcome there means the formalisation succeeded, not that the problem fell. The two are counted separately and never totalled together.

Unproved goals are not a signal

Formal Conjectures is a repository of statements, so sorry is its normal condition and says nothing about whether a problem is open. Formal status is read from the research open and research solved annotations instead. Goal counts are shown as context only.

Scope

The register covers mathematics and theoretical computer science, where a claim can in principle be settled by machine. It does not cover the natural sciences, where it could not.

Exclusions

Bounty platforms settling in testnet tokens are not listed alongside funded prizes. Placing an $86 problem denominated in play money next to a Clay Millennium Prize would misrepresent both.

Corrections

Grades follow mechanically from the rubric above and the source data. If a grade is wrong, then either the source is wrong or the rubric is, and both are public and fixable. Corrections are made in the open, and the underlying dataset is versioned so that any change can be diffed.