FloorCert.lean
The census floor: c_u ≥ 5.021172019×10⁻⁶ for the genuine MT kernel (Real.sin, Real.sqrt 2, π, not a rational surrogate), by explicit rational weak duality plus four kernel bounds proved with…
One person, AI anyone can rent, and a proof checker that accepts no unfinished step. Fulcrum directed the pursuit at a problem open since 1859. Thirteen days later: 4 original theorems accepted by the kernel and a machine-audited candidate past the best published bound. Everything the pursuit produced is below, including what did not work.
| 4 | new theorems |
| 1,145 | kernel-checked theorems |
| 0 | proof gaps |
| 1 | person |
| 13 | days |
| 1,783 | automatic checks |
The Riemann hypothesis says every one of infinitely many special points sits exactly on a particular line. Proving that outright is the open problem, and nothing here touches it. Proving that at least some fraction of them do is the ground people actually gain, and that fraction has been the scoreboard for a century.
On 10 August 2026 an outside paper carried it to 67.25007%.
This laboratory assembled and audited a chain that carries it to
67.25107%, and produced 4 theorems of its
own along the way, each one checked by the Lean kernel with no
sorry, no native_decide and no floating point.
The census floor: c_u ≥ 5.021172019×10⁻⁶ for the genuine MT kernel (Real.sin, Real.sqrt 2, π, not a rational surrogate), by explicit rational weak duality plus four kernel bounds proved with…
The retention certificate's arithmetic: the recorded band-dual cover closes at its four depths, with cap defined by the genuine band supremum and infimum of ω², so the recorded numbers enter only as…
The composition inequality s ≥ 2N − ‖P+Q‖²_F + D, with the corollary that ‖P+Q‖²_F ≤ C·N and D ≥ θ·R₀ give s ≥ (2−C)N + θR₀.
The grid-incidence law Σ_{n∈ℤ} φ̂(x−n)φ̂(y−n) = 2π·FT(φ²)(x−y) for even, bounded, measurable φ supported in [−½, ½]. Continuity is not assumed, which matters: the paper's window jumps at the box edge.
Fractions of a percent are how this problem moves. Each one has taken the field years, and they are argued on paper. This one is machine checked underneath, against the real function rather than a convenient stand-in, which is the shortcut this kind of argument usually takes.
The 67.25007% is Anthropic's, and theirs is much the larger piece of work. A research model running as Claude carried the proven fraction from 41.6% to 67.25007%, with the Lean formalization public alongside it. That is more than twenty-five percentage points on a number the field had been moving in fractions of one. Everything below begins from their theorem and carries it a further one thousandth of a percentage point.
So what this laboratory adds is not size, it is repeatability. Their model has not been released, so the route to their result cannot be re-run from outside Anthropic. This one was assembled two days later from tools anyone can rent. The models are not the unusual part. Fulcrum is.
A laboratory that generates candidates quickly is worth nothing without something that refuses the bad ones, and the refusing is the part that is hard to fake. Two mechanisms do it here.
A proof checker. Lean reads a mathematical argument and
rejects it if a step is missing. That is the strongest guarantee mathematics
has, and until recently getting one meant years of specialist work. So
gaps in the proofs: 0 is not a claim about our confidence, or
a request for yours. It is a machine's verdict, and every result ships with the
#print axioms line that says what it rests on.
That number is about the proofs, not the process. The process is full of guessing: blind alleys, hunches, and prompts that tell a model to behave like a mad scientist and see what falls out. The checker is what makes that a rational way to spend money. It does not care where an idea came from, only whether the argument closes, so you can afford to be reckless at the front of a pipeline when nothing reaches the end of it unproved. Fulcrum directs the pursuit. The checker decides what survives.
A record that keeps what went wrong. 3 claimed results have been withdrawn, each kept with the witness that broke it and the test that now catches it. We have shut down our own flagship tooling on its own evidence, shipped a counterexample the prover found in one of our own statements, and killed a route we proposed ourselves. None of that is written up for this page: the working record is published whole, and readable here rather than on a code host. What did not survive →
The working paper, the obligation ledger, every hunt, every frozen protocol and every correction. Not a summary of them.
181 documents,
45,788 lines, indexed straight off
git ls-files so nothing can be quietly left off, and each one a
page on this site. The library →
Every part of this is available to anyone, which is the point, so it is worth naming which parts carried the weight.
| tool | version | what it did |
|---|---|---|
| Lean 4 + Mathlib | v4.33.0-rc2 | the proof kernel. Nothing counts until it accepts. |
| Aristotle | Harmonic | proof search. Statements are specified here, proofs are machine-found, and the kernel checks them. It also refuted one of our own statements. |
| Arb, via python-flint | 0.6 | ball arithmetic. Carries an enclosure through every step. |
| mpmath | 1.3 | arbitrary precision, the second interval backend, and the independent oracle the suite checks itself against. |
| numpy | 2.0 | bulk statistics |
| scipy | 1.14 | quadrature and interpolation |
| sympy | 1.13 | exact symbolic work |
| Antigravity | agent CLI | sessions across the tree. |
| Claude Code | agent CLI | sessions across the tree, captured in telemetry. |
| Codex | agent CLI | the higher-xi / RAMS2 / RC2 formalization relay. Three modules landed kernel-checked after audit by six independent auditors; nothing was landed on trust. |
A composite claim takes the grade of its weakest step, and nothing here is rounded upward.
sorrys, standard axioms only. These are theorems and are called theorems.What is being worked on right now, read off the branches.
| branch | commits | last |
|---|---|---|
| claude/zeta-constant-improvement-xxnm9a | 16 | 4 hours ago |
| claude/harness-gate | 11 | 23 hours ago |
| claude/o9-first-build | 4 | 10 hours ago |
| hunt/gate5-p6-a | 4 | 11 hours ago |
| hunt/gate5-p6-c | 4 | 12 hours ago |
| hunt/gate5-p6-b | 3 | 12 hours ago |