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.
Throughput is accelerating: 1st contribution July 20th last year, 14 by the end of 2025, 66 by end of Q1 this year, 258 by mid-year, 510 to date with nearly half of this in the last 5 weeks. It’s mostly GPT/Codex-driven. Claude is slowly catching up—I think it’s safe to say the “bad at math” part of Claudiness is no longer true:
Significance vs age at resolution. I wish there was also a “significance frontier over time” view; in lieu of that, here’s a view as of Aug 9th 2026 I spent a few minutes manually compiling:
Significance means: how much did mathematics care about this problem BEFORE it was solved? Score the problem, never the solution—ignore who or what solved it, how elegant the proof is, and any attention the solution itself attracted. A problem’s score is frozen at the moment before its resolution.
Signals that raise the score: named and widely cited conjectures; decades of documented attack and partial results; presence on recognized problem lists (Millennium, Smale, Yau, Erdős’s books and problem collections, Kourovka Notebook); consequences and machinery that other mathematics depends on; fame beyond the originating subfield. Signals that do not raise the score: difficulty alone, age alone, an impressive solution, media coverage of the solve.
Calibrate against this anchored ladder:
100 - Riemann hypothesis. The reference point: a millennium problem with a thousand conditional theorems.
65-70 - Jacobian conjecture: on Smale’s list, notorious across a major field for most of a century.
50-60 - conjectures with textbooks and subfields organized around them (cycle double cover, KLS).
30-40 - field-famous workhorses: known and cited across one research community for decades, invisible outside it (Feige’s conjecture, the Kannan-Tetali-Vempala swap-chain conjecture).
15-25 - established named problems within a specialty; questions with a real literature but a small audience.
10 - a typical numbered Erdős problem or an open question from a specialist paper: real, documented, unfamous.
5 - machine-generated conjectures (Graffiti, TxGraffiti, Written on the Wall) and recent one-paper questions.
0 - reserved; do not use it to mean “unknown”.
Then PLACE the problem against the catalog’s anchor spine. These are real entries whose scores are fixed by editorial decree; every other score is a statement about where the problem sits relative to them:
10 - Erdős Problem #1217, a typical numbered Erdős problem (`erdos-1217`)
5 - Graffiti’s residue problem (`graffiti-residue-common-divisor`)
They’ve been mainly in combinatorics and number theory, but plenty of other areas are represented:
AI has played a leading contribution almost from the get-go:
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.
Problems have been resolved chiefly through conceptual arguments and construction of explicit objects, not finite computation:
There’s a rapidly-growing gap in independent verification, per this chart by u/Bbrhuft (snapshot Aug 6th), who notes that “authors generally include a Lean proof themselves”.
VibeMathed’s verification ladder
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.
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.
Maybe it would be good to know how often the AI co-developed solutions can now be obtained by the latest AI models working on their own. (The checks would need to be limited to problems solved after the knowledge cutoff dates of the latest models, and probably restricted to Lean-verified only.)
That might provide an indicator for when we are starting to exit the centaur phase, at least for the problem solving part of math.
Also, how many of the VibeMath users / contributors do you think are agents? In their dataset, I see only one identifiably human name (JSON key: submittedBy).
While I don’t doubt that progress is accelerating, are you sure it isn’t exaggerated by backfilling problems that were solved before vibemathed.com was created (July 20, according to Google)? Long-term it won’t matter since most problems will be solved after vibemathed was created, but it matters now.
Unrelated, but I’m curious what are everyone’s predictions for when an LLM will solve one of Millennium math problems, or problems of similar caliber such as Collatz or twin primes.
You’ve reminded me that I need to get some fatebook predictions out on the sorts of questions you raised. I’m probably 50⁄50 on “as significant as Collatz by EOY2026” (but not Collatz specifically) by the standards of the significance prompt, haven’t yet thought about the Millennium prize problems enough to bet on.
VibeMathed (GitHub, /api/dataset, methodology, significance auto-scoring prompt) is the best window I know into the industrialisation of pure math problem-solving. Tracking is complete from Nov ’25 onward.
previously in the industrialisation of pure math series
In chronological order:
AI contributions to Erdos problems on Terry Tao’s GitHub
GDM’s Gemini 3.1 Pro-based agent autonomously resolving 9 Erdos problems at a few hundred dollars per problem, out of the full set of 353 in the open-source Formal Conjectures repo
OpenAI Astra’s progress on 10 open problems in math/TCS at $200 per problem
Throughput is accelerating: 1st contribution July 20th last year, 14 by the end of 2025, 66 by end of Q1 this year, 258 by mid-year, 510 to date with nearly half of this in the last 5 weeks. It’s mostly GPT/Codex-driven. Claude is slowly catching up—I think it’s safe to say the “bad at math” part of Claudiness is no longer true:
Significance vs age at resolution. I wish there was also a “significance frontier over time” view; in lieu of that, here’s a view as of Aug 9th 2026 I spent a few minutes manually compiling:
July 20th: 65 - Jacobian conjecture disproof by Claude Fable 5
July 10th: 55 - cycle double cover conjecture by GPT-5.6 Sol (Ultra)
May 2026: 40 - Erdős’s planar unit distance conjecture by an undisclosed OpenAI model
May 11th: 37 - Talagrand’s complexity problem by GPT-5.5 Pro
Significance ladder calibration details
Significance means: how much did mathematics care about this problem BEFORE it was solved? Score the problem, never the solution—ignore who or what solved it, how elegant the proof is, and any attention the solution itself attracted. A problem’s score is frozen at the moment before its resolution.
Signals that raise the score: named and widely cited conjectures; decades of documented attack and partial results; presence on recognized problem lists (Millennium, Smale, Yau, Erdős’s books and problem collections, Kourovka Notebook); consequences and machinery that other mathematics depends on; fame beyond the originating subfield. Signals that do not raise the score: difficulty alone, age alone, an impressive solution, media coverage of the solve.
Calibrate against this anchored ladder:
100 - Riemann hypothesis. The reference point: a millennium problem with a thousand conditional theorems.
85-90 - Goldbach, twin primes, Navier-Stokes regularity: household names beyond mathematics.
~80 - Collatz: enormous fame, structurally isolated.
65-70 - Jacobian conjecture: on Smale’s list, notorious across a major field for most of a century.
50-60 - conjectures with textbooks and subfields organized around them (cycle double cover, KLS).
30-40 - field-famous workhorses: known and cited across one research community for decades, invisible outside it (Feige’s conjecture, the Kannan-Tetali-Vempala swap-chain conjecture).
15-25 - established named problems within a specialty; questions with a real literature but a small audience.
10 - a typical numbered Erdős problem or an open question from a specialist paper: real, documented, unfamous.
5 - machine-generated conjectures (Graffiti, TxGraffiti, Written on the Wall) and recent one-paper questions.
0 - reserved; do not use it to mean “unknown”.
Then PLACE the problem against the catalog’s anchor spine. These are real entries whose scores are fixed by editorial decree; every other score is a statement about where the problem sits relative to them:
65 - Jacobian conjecture (`jacobian-conjecture`)
55 - Cycle double cover conjecture (`cycle-double-cover-conjecture`)
45 - Connes rigidity conjecture (`connes-rigidity-conjecture`)
40 - Erdős’s planar unit distance conjecture (`erdos-planar-unit-distance`)
35 - Feige’s conjecture (`feiges-conjecture`)
30 - Kannan-Tetali-Vempala conjecture (`kannan-tetali-vempala-conjecture`)
25 - The Banks-Martin conjecture (`banks-martin-primitive-sets`)
20 - Babai-Frankl’s Oddtown question (`babai-frankl-oddtown-composite`)
15 - Erdős Problem #1196, primitive sets (`erdos-1196-primitive-sets`)
10 - Erdős Problem #1217, a typical numbered Erdős problem (`erdos-1217`)
5 - Graffiti’s residue problem (`graffiti-residue-common-divisor`)
They’ve been mainly in combinatorics and number theory, but plenty of other areas are represented:
AI has played a leading contribution almost from the get-go:
Problems have been resolved chiefly through conceptual arguments and construction of explicit objects, not finite computation:
There’s a rapidly-growing gap in independent verification, per this chart by u/Bbrhuft (snapshot Aug 6th), who notes that “authors generally include a Lean proof themselves”.
VibeMathed’s verification ladder
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.
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.
Maybe it would be good to know how often the AI co-developed solutions can now be obtained by the latest AI models working on their own. (The checks would need to be limited to problems solved after the knowledge cutoff dates of the latest models, and probably restricted to Lean-verified only.)
That might provide an indicator for when we are starting to exit the centaur phase, at least for the problem solving part of math.
Also, how many of the VibeMath users / contributors do you think are agents? In their dataset, I see only one identifiably human name (JSON key: submittedBy).
While I don’t doubt that progress is accelerating, are you sure it isn’t exaggerated by backfilling problems that were solved before vibemathed.com was created (July 20, according to Google)? Long-term it won’t matter since most problems will be solved after vibemathed was created, but it matters now.
Unrelated, but I’m curious what are everyone’s predictions for when an LLM will solve one of Millennium math problems, or problems of similar caliber such as Collatz or twin primes.
Yup (unless I’m misreading you):
You’ve reminded me that I need to get some fatebook predictions out on the sorts of questions you raised. I’m probably 50⁄50 on “as significant as Collatz by EOY2026” (but not Collatz specifically) by the standards of the significance prompt, haven’t yet thought about the Millennium prize problems enough to bet on.