Methodology

We grade every finding as one record on two axes: how solid the evidence is and how much the AI actually did. Grades are set conservatively and only ever downgraded, never quietly removed.

Verification: how solid is it?

We order these strongest to weakest. When we're unsure, the lower grade wins.

Formally verified

A machine-checked proof (Lean, Coq, Isabelle) or an exact symbolic or computational verification that anyone can rerun. The gold standard.

Independently checked

Multiple qualified people unaffiliated with the announcing lab have checked the result and confirmed it.

Peer reviewed

Published in a venue with real review. Weaker than a formal proof for mathematics, but stronger for empirical claims.

Author verified

The human collaborator checked it, but no independent party has confirmed it yet.

Claimed

Announced but not yet checked by anyone outside the lab. The default for a press release.

Disputed

Substantive technical objections have been raised and remain unresolved.

Already known

The result turned out to already exist in the literature. These entries stay on the record; showing the failure mode is what makes the rest trustworthy.

Refuted

Shown to be wrong.

Autonomy: how much did the AI do?

This axis is the whole point. Most breathless claims collapse here; we grade on the strictest defensible reading.

Autonomous

The AI produced the core idea and the result with no human mathematical input beyond posing the problem.

AI-led

The AI produced the key insight; humans formalised, checked, or cleaned it up.

Collaborative

Genuine back-and-forth. Neither party would have gotten there alone.

AI-assisted

A human drove the research; the AI accelerated search, algebra, or literature review.

Search scaffold

The AI is a component inside a human-designed search loop (FunSearch, AlphaEvolve). The system found it, but the framing was human.

Retrieval

The AI surfaced an existing result humans had overlooked. Valuable, but not new mathematics.

The two are independent. A result can be formally verified and barely autonomous, or autonomous and merely claimed. Reading one grade without the other is how a press release becomes a discovery.

What each source is

Every link on an entry is one of five things, sorted by what the link does rather than who published it. Keeping them apart is the point: most of the distance between a result and a headline is in the last four. A lone researcher announcing their own result is an announcement exactly as a corporate press release is.

Original work

The work itself: a paper, preprint, formal proof, dataset or code repository - something a reader can open and check. Not what was said about the work, but the work. Any grade stronger than Claimed has to rest on one of these.

Announcement

The claim as first made public by the people behind it - a company press release, a research blog post, or an individual's own post on a personal site or social media. What matters is that it is first-party, not that an organisation published it: a single researcher announcing their own result belongs here. This is the claim framed by the people with the most at stake in it.

Media coverage

News and press reporting written by journalists rather than by the people who did the work. Coverage restates a result for a general audience, and the restatement is often where it acquires a stronger meaning than its authors gave it.

Independent commentary

An independent write-up by someone who neither produced the result nor is reporting it as news - a researcher's blog post, an expert explainer, a detailed thread. Often the most informative link on an entry. It may support the claim, complicate it, or both; commentary arguing the result is wrong is a challenge instead.

Challenge

The case against: a critical review, a rebuttal, a failed replication, or a citation of prior work showing the result was already known. The strongest challenge is listed first. A challenge disputes the claim, not the people who made it.

Editorial rules

These are what separate the registry from a press-release aggregator.

  1. We run a novelty check before publishing, no exceptions. What was searched gets recorded even when it comes back clean.
  2. We never delete an entry. We downgrade and annotate it instead; the public history is the credibility mechanism, and quiet edits destroy it.
  3. We cap a claim with no reproducible artifact at claimed. No exceptions for famous labs.
  4. We start lab-announced results at claimed regardless of how confident the announcement sounds.
  5. We grade autonomy on the strictest defensible reading. If a human posed the problem, suggested the approach, and checked the algebra, that is not autonomous.

Other registries

Where another project holds a record of the same result, entries cite it and say what it establishes. None of these grades autonomy, and none keeps refuted results.

PalomarA Lean proof that typechecks against the recorded statement at a pinned commit under a declared axiom set, checked mechanically rather than by human review. It does not certify that a result is new or of research interest: the only filter on that is a language-model screen, and Palomar states that it adds no human editorial step.
ProofAtlasThat a recorded Lean build passed with no unfinished proof steps, under its own evidence contract, which a record can satisfy for checking while still failing for acceptance.
MathDBNothing mechanically. It records what a problem says, what is known about it, and the standing of any claimed solution.
vibemathedNothing mechanically. It is a parallel listing of the same result, carrying its own verification label rather than an independent check.

What each one certifies →