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 that do not resolve a stated question.

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.

Every entry carries a result - proved or disproved - 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. 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: inside the formal statement, the argument has no gaps at all. What the kernel cannot check is the translation, whether that formal statement really is the problem as posed, so a human still has to confirm the two match. 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.

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.

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, from 0 to 100 in steps of 5. 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.

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.

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.

Everything on this site is free to reuse under CC BY 4.0, and 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.