Verification tiers: Peer-reviewed traditional human review of a written proof  ·  Computer-assisted machine computation essential; programs human-checked  ·  Formally verified every logical step machine-checked in a proof assistant (Lean / Coq / Isabelle / HOL Light) — the strongest guarantee mathematics currently offers.

Machine-readable version of this entire board: registry.json

🔓 Open Problems (9)

Unresolved as of this build. Computational evidence, however extensive, is not proof — see the Mertens Conjecture below for why.

ProblemPosedPosed by
Riemann Hypothesis
All non-trivial zeros of the zeta function have real part 1/2.
🏅 Clay Millennium Prize ($1M) — open. Also Hilbert Problem 8.
First 10 trillion+ zeros verified computationally to lie on the critical line — strong evidence, not proof
1859 Bernhard Riemann
Collatz Conjecture
Iterating n -> n/2 (even) or 3n+1 (odd) always reaches 1.
Verified computationally for all starting values up to ~2^68; Tao (2019) proved 'almost all' orbits reach almost-bounded values
1937 Lothar Collatz
Goldbach Conjecture (strong form)
Every even integer greater than 2 is the sum of two primes.
Weak (ternary) form — every odd number >5 is a sum of three primes — proven by Harald Helfgott (2013, widely accepted). Strong form verified computationally to 4x10^18.
1742 Christian Goldbach (letter to Euler)
Twin Prime Conjecture
There are infinitely many primes p such that p+2 is also prime.
Major progress: Yitang Zhang (2013) proved bounded gaps (70 million); Polymath8b reduced the bound to 246
1849 (de Polignac, general form) Alphonse de Polignac
P vs NP
Can every problem whose solution is quickly verifiable also be quickly solved?
🏅 Clay Millennium Prize ($1M) — open
1971 Stephen Cook (independently Leonid Levin)
Navier–Stokes Existence and Smoothness
Do smooth solutions to the 3D Navier-Stokes fluid equations always exist for all time?
🏅 Clay Millennium Prize ($1M) — open
19th century (equations); 2000 (formal problem statement) Clay Mathematics Institute (formal statement by Fefferman)
Hodge Conjecture
Certain topological classes on projective algebraic varieties are combinations of algebraic cycle classes.
🏅 Clay Millennium Prize ($1M) — open
1950 W.V.D. Hodge
Birch and Swinnerton-Dyer Conjecture
The rank of an elliptic curve's rational points is determined by the behaviour of its L-function at s=1.
🏅 Clay Millennium Prize ($1M) — open
1965 Bryan Birch and Peter Swinnerton-Dyer
Yang–Mills Existence and Mass Gap
Prove quantum Yang-Mills theory exists rigorously on R^4 and has a positive mass gap.
🏅 Clay Millennium Prize ($1M) — open
2000 (formal problem statement) Clay Mathematics Institute (formal statement by Jaffe and Witten)

✅ Proven (9)

ResultResolvedByVerification
Basel Problem
Sum of reciprocal squares 1 + 1/4 + 1/9 + ... equals pi^2/6.
1734 Leonhard Euler (rigorous proof 1741) Peer-reviewed
Abel–Ruffini Theorem
No general algebraic formula (in radicals) exists for polynomial equations of degree 5 or higher.
1824 Niels Henrik Abel (Ruffini's 1799 proof was incomplete) Peer-reviewed
Prime Number Theorem
The number of primes below x is asymptotically x/ln(x).
Formally verified: elementary proof in Isabelle (Avigad et al., 2004); analytic proof in HOL Light (Harrison, 2009)
1896 Jacques Hadamard and Charles de la Vallée Poussin (independently) Formally verified
Gödel's Incompleteness Theorems
Any consistent formal system containing arithmetic has true statements it cannot prove; no such system can prove its own consistency.
Formally verified in multiple systems (e.g. Paulson in Isabelle, 2013; O'Connor in Coq, 2005)
1931 Kurt Gödel Formally verified
Nash Equilibrium Existence Theorem
Every finite game has at least one equilibrium in mixed strategies.
1950 John Nash Peer-reviewed
Four Colour Theorem
Every planar map can be coloured with at most four colours so no adjacent regions share a colour.
Originally computer-assisted (1976); fully formally verified by Georges Gonthier in Coq (2005)
1976 Kenneth Appel and Wolfgang Haken Formally verified
Fermat's Last Theorem
No positive integers a,b,c satisfy a^n+b^n=c^n for integer n>2.
Full formalization in Lean in progress (project led by Kevin Buzzard, begun 2024)
1995 Andrew Wiles (with Richard Taylor) Peer-reviewed
Kepler Conjecture
No sphere packing in 3D exceeds density pi/sqrt(18) ~= 74.05% (cannonball stacking is optimal).
Originally computer-assisted (1998, published 2005); fully formally verified by the Flyspeck project in HOL Light and Isabelle (2014)
1998 Thomas Hales Formally verified
Poincaré Conjecture
Every simply connected closed 3-manifold is homeomorphic to the 3-sphere.
2003 Grigori Perelman (verification by independent teams completed 2006) Peer-reviewed

❌ Disproven (2)

Conjectures that turned out to be false — including one supported by enormous numerical evidence before its disproof.

ConjectureDisprovenByMethod
Mertens Conjecture
The Mertens function M(n) is bounded by sqrt(n) in absolute value for all n>1.
Disproven via computational analysis of zeta zeros — no explicit counterexample n is known even today. A cautionary tale: extensive numerical evidence suggested it was true, and its truth would have implied the Riemann Hypothesis.
1985 Andrew Odlyzko and Herman te Riele Computer-assisted
Euler's Sum of Powers Conjecture (entry pending)
At least n nth powers are needed to sum to an nth power (generalising Fermat).
Disproven by direct computer search: 27^5 + 84^5 + 110^5 + 133^5 = 144^5. The published paper is famously only two sentences long.
1966 L.J. Lander and T.R. Parkin Computer-assisted

⚖️ Independent of the Axioms (1)

A fourth possibility most people never learn exists: statements that can neither be proven nor disproven from the standard ZFC axioms of mathematics.

StatementEstablishedByVerification
Continuum Hypothesis
There is no set whose cardinality lies strictly between the integers and the real numbers.
Neither provable nor disprovable from the standard ZFC axioms — a fundamentally different kind of resolution. Hilbert Problem 1.
1963 Kurt Gödel (1940, consistency) + Paul Cohen (1963, independence; Fields Medal 1966) Peer-reviewed
Maintenance policy: this board is regenerated from registry.json — the single source of truth — at every codex build. Every Theorem-type entry added to the codex receives a registry row. Status changes (a proof announced, verified, or retracted) are recorded with sources; announcements are not marked "proven" until peer review or formal verification completes.