Methodology

The inclusion test is one sentence: a precisely stated open question whose answer is now a proved or disproved theorem, with an AI model substantively in the loop. Any field of mathematics qualifies, theoretical computer science included - a complexity-theory theorem is as much mathematics as a number-theory one.

Deliberately out of scope: formalizations of results humans had already proved (formalizing a 1963 proof is valuable, but it is not a problem no human had solved), empirical results such as cryptanalytic attacks with measured work factors, and heuristic or record-improving constructions on a quantity nobody tracks. A proof that merely reproves something already settled without AI is out too, because it cannot be shown to be independent of the work it follows.

Concurrent independent proofs are the exception to that last rule. When two proofs of the same problem appear within weeks by demonstrably different methods, and the authors state they worked independently, the later one is not derivative work: it is ordinary mathematics, which has always produced simultaneous discoveries. An AI-assisted proof in that situation stays in the record, because a model genuinely contributed to proving the thing. What such an entry may not do is imply a priority it lacks, so it names the competing proof in its result note, links it, and says plainly that the first proof of the problem may not have been the AI-assisted one. Crouzeix's conjecture is the worked example.

Extraordinary claims are held, not listed. A claim that would be a major result by any expert's standard - a famous conjecture, a problem with decades of failed attempts, an object the field expected not to exist - is not published at Unreviewed, and not published as a Candidate either, because a listing here puts the site's name beside a claim it has not read. It waits until a named expert with no stake in it has checked the argument or a formal proof exists, and the submitter is told so in as many words, with the way back. The test is the size of the claim, not the credentials behind it: the rule is the same for a preprint by known authors and for an anonymous agent. This record is not where a landmark result is announced; it is where the announcement is recorded once it has stood up.

Three ways: marquee results curated by hand; Erdős-problem solves imported from Terence Tao's AI-contributions wiki (full solutions only, each verified against its erdosproblems.com page); and reader submissions, which are reviewed before publishing and credited to the submitter by pseudonym. Every entry must cite a real, checkable primary source.

Sweeps of machine-generated conjectures - Graffiti, Written on the Wall, TxGraffiti - are now refuted by agents by the hundred. Each one is a stated open question with a checkable answer, so each one qualifies, and each one scores 5. They enter the record one entry per conjecture, as the Erdős problems do, so the dataset stays one row per problem and a later submission of the same conjecture is caught as a duplicate. Three conditions: every entry is Site-confirmed or better, its certificate re-run here or its proof machine-checked, because an unreviewed batch is not a record of anything; a sweep is imported as a batch by a curator from the repository's own manifest rather than filed one form at a time; and every entry names its sweep as the source, so the sweep can be read as a whole. Volume is handled by the significance score, which is a sort and a filter, not by leaving qualifying results out.

Every entry carries a result - proved, disproved or independent - and a status saying what actually happened to the problem:

Resolved

The stated problem is fully proved or disproved.

Partial result

A real advance - a new bound, a resolved special case - but the problem itself remains open.

Variant only

Only a variant, or a literal reading of the historical wording, was resolved.

Candidate (review pending)

A full solution is claimed and publicly checkable, but authoritative review (a community tracker, referees) is still pending.

Retracted

The claim was withdrawn or refuted after publication. Kept on record, not deleted.

The result records the fate of the statement as it was posed- a proof of X is logically a disproof of not-X, so proved versus disproved tracks whether the community's expectation held, not a property of the mathematics.

Independent is a third outcome rather than a variety of the first two. The statement is neither provable nor refutable from the ambient axioms, and that is itself the theorem. Recording such a result as proved would describe the metatheorem rather than the problem, and recording it as disproved would describe nothing at all, so the axis has three values. The problem still counts as resolved: the answer to “which is it?” turned out to be “neither, provably”, which is an answer.

What the resolution actually consisted of is the method:

Construction

An explicit object settles it: a counterexample, a witness, a presentation. Classified by the decisive step per the source.

Computation

A finite certificate or an exhaustive case analysis carries the result - neither an object nor a theory.

Argument

A conceptual proof: the resolution is an idea, not a search hit.

Separately, an entry can carry a claim issue: a documented problem with the claim itself, such as a refuted lemma or a misformalized formal statement. Claim issues render as a visible flag, never as a silent deletion.

Disclosures range from "the proof is found by the model" to "the model helped with one lemma", and those must not carry the same weight. Every new entry is classified by degree of AI involvement, strongest first:

AI-discovered

The model produced the central proof or object - the counterexample, the construction, the argument - and humans verified and wrote it up.

AI co-developed

Named, essential steps came from the model inside a human-led proof: a key lemma, a construction idea, a subproblem the authors formulated and the model solved.

AI-assisted

Instrumental but human-led: the model built the search or verification tooling, checked proofs, or otherwise contributed work the authors call material to the result.

Below the bottom tier there is no tier: papers where AI only wrote, proofread, drew figures or ran routine code checks are out of scope entirely - as is any paper whose authors state the mathematics is theirs alone. Classification takes the authors' own disclosure at face value, and a vague disclosure gets the lower tier. Entries added before this axis existed are unclassified until reviewed; an unclassified entry says nothing about the degree of involvement.

Status says what happened; verification says how the mathematics was checked. The tiers run strongest to weakest with one deliberate exception: the top two are not comparable. A Lean kernel and an independent expert catch different mistakes, so an entry at either tier is well checked, and the rare entry at both is as good as this record gets.

Lean-verified

A formal proof machine-checked end to end by the Lean kernel, AND the formal statement independently anchored: the canonical tracker accepted the claim, the statement is pinned in a community-reviewed repository such as Formal Conjectures, or someone with no stake in the proof audited the informal-to-formal correspondence. Both halves are required, because the kernel checks the proof against the supplied statement and nothing can make it check the statement against the problem as posed. Entries checked modulo explicitly named literature inputs, or leaning on native_decide, say so in their verification note.

Independently expert-verified

Checked and endorsed by named domain experts with no stake in the claim. Slower and much rarer than formalization, and it catches what a kernel cannot: a formal statement that drifted from the informal problem, a result already sitting in the literature, a proof that answers the neighbouring question. The authors checking their own work does not count, however expert they are, and that stays Unreviewed.

Site-confirmed

Either the canonical community tracker accepted the claim - for Erdős problems, erdosproblems.com marks it solved - or this site reproduced the artifact itself: re-ran a finite certificate, re-derived a counterexample in exact arithmetic, rebuilt a formalization and audited which axioms its theorem really uses. The entry's verification note always says which of the two happened, and exactly what was run.

Lean-checked, statement unaudited

The Lean artifact compiles with no sorry and no stray axioms, but nobody independent has audited whether the formal statement faithfully expresses the original conjecture - typically because the same system produced both the proof and its formalization. A valid kernel check of an unaudited statement can still concern a nearby, weakened or otherwise unintended claim, and statement fidelity is exactly where an autonomous prover is most likely to fail silently. This tier used to be folded into Lean-verified; splitting them is what makes the top rung mean what it says.

Unreviewed

Nobody independent has checked the mathematics yet, whatever venue the claim lives in.

Contested

Actively disputed, walked back, or withdrawn outright. The entry stays listed so the dispute is on record.

A listing in the Palomar registry is recorded on an entry when it exists, and it is worth saying exactly what it buys. Palomar requires the Lean FRO's comparator, which forces the statement of a theorem to be separated from its proof and to depend on Mathlib alone. That turns “clone the repository and work out which files you have to trust” into something a stranger can check in a minute, which is the practical obstacle that has kept most formalized entries at Lean-checked rather than Lean-verified.

What it does not do is decide whether the formal statement says what the informal problem said. Palomar states plainly that a listing “does not constitute a certificate of novelty, nor a certification of relevance”, and separating a statement from a proof does not make that statement faithful. So a listing is treated here as a strong precondition rather than as the anchoring itself: it makes the audit cheap, someone still has to do it.

Peer review is deliberately not a rung on this ladder. It answers a different question, where the claim sits in the scholarly pipeline, and every entry records that separately. The two axes are independent, and a Lean-verified result can sit in a bare company announcement. Most currently do: journals move far slower than these results arrive, which is exactly why refereeing cannot be the spine of this scale.

Announced

The claim lives in a blog post, a repository, a tracker page or a social post - no manuscript venue.

Preprint

A manuscript on arXiv or a similar server, not yet refereed.

Peer-reviewed

Accepted by a journal or a conference.

Status, verification and publication are editable by signed-in readers, because they genuinely change over an entry's life - a preprint gets refereed, a candidate gets accepted, a claim gets walked back. Changing any of them requires updating the verification note in the same edit, and every change lands in the entry's public changelog.

Every entry carries an AI-estimated significance score: how much mathematics cared about the problem before it was solved, as an integer from 0 to 100. It is calibrated against an anchored ladder - the Riemann hypothesis is 100, Collatz sits near 80, the Jacobian conjecture near 65, a conjecture famous within one research community around 30, a typical numbered Erdős problem around 10, and machine-generated conjectures around 5 - and, since v2 of the scoring prompt (August 2026), each score is placed comparatively against a fixed spine of catalog entries whose scores are frozen by editorial decree. A single problem judged in isolation is only honest to a band of about five points; one-point resolution comes from answering "above or below that one?" against named neighbours. Ties are deliberate: problems of genuinely similar standing share a score rather than being forced into spurious distinct integers. The whole catalog was rescored under v2 on 6 August 2026.

The score is a curator measurement, never self-reported: it is assigned at review time by an AI model applying a fixed rubric, with a one-line justification stored on the entry, and the whole catalog gets a pairwise consistency sweep. The score describes the problem as it stood before its resolution, so attention triggered by the solution itself can never inflate it. Scores are editorial estimates, stable to within a band - challenge one in the entry's discussion thread. The verbatim scoring prompt is public: significance-prompt.md, versioned in the repository; any wholesale rescore is documented there.

One cluster gets a further, evidence-based pass rather than resting on comparative judgment alone: the numbered Erdős problems, which made up two large ties at the bottom of the scale. Erdős priced the problems he cared most about himself, in dollars, and erdosproblems.com records how much literature and discussion each one has attracted - both are real per-problem signals, not guesses. On 6 August 2026 every numbered entry was checked against both: a documented prize or an unusually dense reference trail moved a problem up within its band. This is promotion-only - a thin page is evidence of nothing, not of insignificance - and the large tie that remains after this check is stamped as examined (each such entry's note says so explicitly) rather than left as an unexamined default. A shared score should mean "checked and found comparable," never "never looked."

Wikipedia language editions with an article about this specific problem. Generic concept articles don't count, and an article that exists only because the problem was solved does not count either. 0 means no such article.

The count is a frozen snapshot on purpose: coverage triggered by the solution itself can never inflate a problem's fame after the fact. It now lives as a supporting fact on entry pages - most genuine AI solves score zero, which is itself a finding - while the headline metric on cards is the significance score, which the Wikipedia count keeps honest: a high score beside "no dedicated article" is a visible tension anyone can challenge.

The posed year is the earliest cited reference for the problem, so ages are close estimates rather than exact anniversaries. Entries where the span oversells how fully the problem is closed carry a footnote next to the age.

Some questions are not answered, they are approached. The exponent of matrix multiplication has been creeping since 1969 and will not stop at a theorem; the proportion of zeta zeros proved to lie on the critical line went from a third to two thirds over fifty years. For those, a single entry says almost nothing on its own. A frontier is the named quantity itself, with a direction and the sequence of best known values, and the entry becomes one step on it.

A frontier exists only once a catalog entry sits on it. That is the rule that keeps this site what it is. The historical steps are there as context for an AI result, not as content in their own right, and this is not a general leaderboard of human mathematics. Every historical row cites the source its value was read from, and where that source is a later paper's account of what it improved rather than the original, the frontier's history note says so.

The current best is derived, never declared. A frontier stores a direction and its rows; which row leads follows from those two things. A row marked a candidate is drawn but never counted: that is where a claim sits when it has been catalogued as an entry but the field has not accepted it as the frontier, which is a statement about what other mathematicians have said, not about how much this site believes it.

This also settles something the scope rule above left ambiguous. A record-improving result on a quantity the field tracks is in scope and is listed as Partial, because there is a stated question with a published sequence of answers and this is the next one. A frontier improvement on a quantity nobody tracks is not, because there is no question, only a bigger example. Whether a frontier exists is the test.

Frontiers are curated rather than submitted. The judgement they need - which quantity, which direction, which rungs are real - is not something a submission form can ask for, and a wrong historical row is a claim about somebody else's mathematics. If an entry belongs on a frontier that does not exist yet, say so in the submission and it will be considered.

What this site wrote - the classifications, the scores, the notes, the structure - is free to reuse under CC BY 4.0. Quoted material from the papers is not ours to license and stays with its authors; the licensing page draws the line. The complete, always-current dataset is one request away: vibemathed.com/api/dataset (JSON, every published entry with all fields). Spotted an error? Every entry has an edit button and a discussion thread, or you can submit a solve we are missing.