AWESOME AI PROOFS
Mathematics & statistics

Catalogue overview

Explore the listed problems by year, subject, model and reported evidence.

153 records

Counts describe this catalogue, not model success rates. Select a bar to see its records. Status and model counts can overlap.

Records by year

Year of the reported event; ranges use their final year.

Reported evidence

A record can have more than one status.

Models and AI systems

A record can credit several systems.

Mathematical subjects

A record can belong to several subjects.

All records

153 records

Definitions and documentation

How the charts count records

Each record represents a problem, a specified variant or an evaluation question. A record appears once per applicable year, model, subject or evidence label. Year ranges use their final year. Multiple labels can apply, so chart totals may exceed the number of records. Chart selections filter the record list; the type control updates all charts.

These counts measure catalogue coverage. They do not measure model success rates, research importance or total mathematical output. Most source collections omit unsuccessful attempts.

Reported evidence

Green and red flags identify verified and debunked reports. Other statuses use separate colours and symbols. Where a label concerns an audit or novelty claim, that scope appears in the badge. A problem with multiple attempts may have several statuses; its page keeps those attempts separate.

Formal artifacts and source review

A proof artifact should identify the statement, theorem file, revision, checker version and build procedure. Assumptions, partial coverage and use of native_decide belong in the entry’s additional information. Statement correspondence and kernel checking are separate checks.

A source-review date records reading the source, not rebuilding its proof or independently certifying its mathematics. Entries without such a review retain a pending date. The model column lists the reported system; unreleased systems may use a company name. “Not specified” means the source notes did not identify the system.

Extraction notes

Multi-result papers were separated into individual statements or named variants. AlphaProof Nexus’s public directory lists nine Erdős files and 38 OEIS files; the original notes report 44 OEIS results. File counts and theorem counts are different units. The catalogue indexes the identified files and does not create unsupported entries to match the headline total.

The 2025 GPT-5 Erdős announcement concerned already published solutions. Its coverage is retained here because the original notes do not identify the ten individual problem numbers. It is not counted as a separate research problem. The original notes remain in the repository archive.

Problem explanations

Collatz: an invalid machine-checked disproof

An intuitive picture

Start with a positive integer. If it is even, halve it; if it is odd, multiply it by three and add one. For example, 3 leads to 10, 5, 16, 8, 4, 2, 1. The conjecture asks whether every positive starting value eventually reaches 1.

What failed in this episode

A purported formal disproof passed vulnerable checkers. The maintainer’s postmortem describes an implementation flaw in Lean and a separate flaw in an outdated independent checker. This invalidated the certificate, not the Collatz conjecture.

A successful build must be tied to checker versions and the exact statement being checked. An absence of sorry is only one part of that record.

Problem and sources →
Feige’s small-deviation conjecture

An intuitive picture

Suppose several independent nonnegative quantities each have mean at most one. Add them up. Even if individual quantities sometimes spike, how much probability must remain below the total mean plus a slack δ?

The scope of the claim

The preprint abstract gives a sharp lower bound when δ ≥ 1 and credits ChatGPT 5.6 Pro with the proof. The catalogue keeps the paper’s range separate from the original notes’ report that the Lean artifact covers δ = 1. Source reading here did not include rebuilding that artifact.

Problem and sources →
Fewer multiplications for 4 × 4 matrices

An intuitive picture

The usual recipe for multiplying two 4 × 4 matrices uses 64 scalar multiplications. Clever rearrangements can reuse intermediate products. The question is how many products suffice for an exact recipe that works for every pair of input matrices.

Why the field matters

Arithmetic modulo two has 1 + 1 = 0. An identity that exploits this cancellation need not work for real or complex numbers. Compare algorithms over the same field before comparing their multiplication counts.

The AlphaTensor paper reports a 47-product algorithm over F₂. This is a construction giving an upper bound on the required number of multiplications, not a proof that 47 is minimal. Later characteristic-zero claims are recorded as separate events below.

Problem and sources →
Large cap sets in eight dimensions

An intuitive picture

Imagine a grid whose coordinates are 0, 1 or 2, with arithmetic wrapping around modulo three. Choose some grid points while avoiding every line of three distinct points. A cap set is a selection with no such triple. In eight dimensions the grid has 3⁸ points; the challenge is to keep as many as possible.

What the AI contribution means

FunSearch searches for programs that construct good selections. Its reported 512-point example proves that the maximum is at least 512. It does not prove that a larger example is impossible. The original paper describes the construction and the human interpretation of the generated program.

Problem and sources →
Tools, benchmarks and related links

Tools and benchmarks

Supporting links from the original notes. Availability and performance figures have not been rechecked.

  • DeepSeek-Prover-V2 (2025) - open-weights Lean prover; the 671B model reaches 88.9% on miniF2F-test at pass@8192. Paper. [machine-checked]
  • Goedel-Prover-V2 (2025) - open-weights Lean prover with verifier-guided self-correction; 88.1% on miniF2F-test at pass@32 with a 32B model, 90.4% with self-correction. Paper. [machine-checked]
  • Kimina-Prover (2025) - formal reasoning model trained with RL; the 72B release reaches 84.0% on miniF2F-test at pass@32. Preview paper; no paper yet for the full model. [machine-checked]
  • Archon (2026) - open dual-agent system (planner plus Lean agent) for formalizing research-level mathematics; reported to have fully automated the formalization of First Proof Problem 6. The open counterpart to the closed AxiomProver and Gauss. [machine-checked]
  • Tau Ceti (2026) - an AI-authored Lean library downstream of mathlib: humans write the roadmaps and review rubrics, AI agents write the code and drive the review, an arrangement the project states plainly. [machine-checked]
  • Lean 4 and mathlib - 280,000+ formalized theorems as of mid-2026; where most machine-checked AI proving happens today.
  • PutnamBench - formalized Putnam problems in Lean 4, Isabelle and Coq.
  • FrontierMath - undergraduate-to-research-level problems, mostly private apart from a twelve-problem public sample; v2 (June 2026) corrected errors in 42% of the original set, so name the version alongside any score.
  • LeanDojo-v2 - framework for training, evaluating and deploying Lean 4 provers, and the maintained successor to LeanDojo, whose last release predates current Lean.
  • First Proof - unpublished research-level problems from working mathematicians, one-shot with no human interaction, double-blind graded by paid human referees; batch 2 used 30 referees grading in person at Harvard CMSA.
  • lean-eval - the Lean team's comparator-based benchmark and leaderboard: a problem counts as solved only if comparator accepts the submission, and every solution is replayed through nanoda, an independent kernel.
  • Formal Conjectures - 2,615 statements formalized in Lean 4, of which 1,029 are open research conjectures. Statements are formalized before any solution exists, which reduces contamination without ruling it out, and is the place a conjecture gets written down before anyone has an answer.
  • MathArena - independent competition evaluation from ETH Zurich and INSAIT. Its Putnam run was graded blind by the official Putnam committee; on its ArXivLean set every model, Aristotle included, scored below 20% as of mid-2026.
  • IMProofBench - 77 research-level problems with expert human grading of full proofs, not just final answers.
  • DL4TP - deep learning for theorem proving; survey paper (COLM 2024). Paper list stops at May 2025.