Catalogue overview

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.

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.

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.

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.

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.

• miniF2F - olympiad-level formal benchmark; the original repo is archived, so use a corrected variant: miniF2F-v2 (data, audit paper) or facebookresearch/miniF2F. Scores are not comparable across variants.

• 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.

• AI contributions to Erdős problems - community registry of AI results on Erdős problems; frozen 30 June 2026, no longer updated.