A living record of AI-assisted mathematics
VibeMathed is the first site to track mathematical problems solved by AI across all of mathematics — from famous conjectures to the long tail of specialist questions.
Famous Conjectures
Long-standing open questions that have shaped entire fields — such as the Jacobian conjecture — now resolved with AI models substantively in the loop.
Numbered Erdős Problems
The catalogued problems from Paul Erdős's legacy, tracked against canonical sources like erdosproblems.com and imported via Terence Tao's AI-contributions wiki.
Open Challenges
Specialist questions across number theory, graph theory, combinatorics, analysis, and theoretical computer science — any precisely stated theorem whose resolution involved AI.
What qualifies
The inclusion test is strict: a precisely stated open question whose answer is now a proved or disproved theorem, with an AI model substantively in the loop. Theoretical computer science is treated equally alongside number theory or analysis.
What is excluded
Formalizations of already-settled results, empirical cryptanalytic attacks, heuristic constructions without a stated resolution, and papers where AI only wrote text or ran routine checks.
How results are tracked
Every entry is classified rather than merely listed. Status, verification, AI contribution, and publication are tracked as independent axes.
Verifiable Sources
Every entry cites a real, checkable primary source. Entries come from hand-curated marquee results, Terence Tao's AI wiki, and reviewed reader submissions.
Result & Status
Each entry carries a result (proved / disproved) and a status: Resolved, Partial result, Variant only, Candidate, or Retracted.
Global Tracking
The record is fully open and editable by signed-in readers. Every change lands in a public changelog. The complete dataset is available under CC BY 4.0.
AI Contribution Levels
AI-discovered
The model produced the central proof, counterexample, or construction. Humans verified and wrote it up.
AI co-developed
Named, essential steps came from the model inside a human-led proof — a key lemma, construction idea, or subproblem the model solved.
AI-assisted
Instrumental but human-led. The model built search or verification tooling, checked proofs, or otherwise contributed materially.
The verification ladder
Verification is tracked independently from publication status. Peer review answers a different question — where a claim sits in the scholarly pipeline — so it is recorded separately.
Lean-verified
Machine-checked end-to-end by the Lean kernel, with the formal statement independently anchored against the original problem.
Formal + AuditedIndependently expert-verified
Checked and endorsed by named domain experts with no stake in the claim. Catches what a kernel cannot: drifted statements, duplicate literature, neighbouring questions.
Human ExpertSite-confirmed
The canonical community tracker accepted the claim, or the site reproduced the artifact: re-ran a certificate, re-derived a counterexample, or rebuilt a formalization.
Community / ReproducedLean-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.
Formal OnlyUnreviewed
Nobody independent has checked the mathematics yet, whatever venue the claim lives in.
PendingContested
Actively disputed, walked back, or withdrawn outright. The entry stays listed so the dispute is on record.
DisputedSignificance scoring
Every entry carries an AI-estimated significance score from 0 to 100, calibrated against an anchored ladder. The score describes how much mathematics cared about the problem before it was solved.
Scores are editorial estimates assigned at review time by an AI model applying a fixed rubric, with a one-line justification stored on each entry. The whole catalog undergoes pairwise consistency sweeps. 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.
Open data, open code, open history
VibeMathed is not merely a list. It is a rigorous, transparent, and community-governed historical record of AI's growing role in advanced mathematics.
Free to Reuse
The complete dataset is available under CC BY 4.0 at /api/dataset. The source code is public on GitHub under an open license.
Oldest Problem Cracked
Schiffer's Conjecture, posed in 1929, is the oldest problem in the record to have been resolved with AI assistance — 97 years open.
Community Curated
Submitted, reviewed, and curated by a community that cares about getting the mathematics right. Every entry has a public changelog and its own discussion thread.