A hard result, produced with AI assistance, in a field where reviewers are right to be skeptical — and finished as an artifact a machine checks line by line rather than a claim anyone has to take on trust. The work spanned a dozen sessions with no shared memory between them. What made that survivable was not the mathematics; it was the board holding what was proved, what was still assumed, and which approaches had already failed.
Producing results is no longer the bottleneck. Establishing which ones survive scrutiny is.
The 3x+1 research program produced a chain of analytic estimates — a "δ=1 certificate" — resting on three technical lemmas. The chain was written by hand, assisted by AI, and concerned territory adjacent to the Collatz conjecture. That last detail matters: the field has seen enough confidently-wrong AI-assisted proofs that a reasonable mathematician's prior on a new one is low, and human referee time runs to months.
This is the general case, not a quirk of number theory. Any group using AI in its research now faces the same question from reviewers, funders and its own PI: how do we know? A chat transcript is not an answer. Neither is a confident summary.
An external mathematician's advice was blunt: don't ask people to trust it — make it checkable. Formalise it in Lean, where a computer verifies every inference and the trust boundary is explicit rather than rhetorical. That advice arrived as a message and left as a ticket, re-prioritised to P1 — which is the first thing worth noticing about the board's role here. Outside input became scoped, tracked work instead of a conversation someone remembers.
Lean tracks which axioms every theorem depends on. Ordinary mathematics rests on three —
propext, Classical.choice, Quot.sound. A fourth,
sorryAx, appears when a proof leans on something admitted rather than proved.
A theorem carrying sorryAx proves nothing at all. Everything below is about
driving that count to zero and being able to demonstrate it.
Not storage. Decomposition, sequencing, and memory.
The mathematician's recommendation became ticket TXPOF-59 with an explicit three-phase plan: prove the exact lemmas, then the reduction skeleton, then numeric bridging. Phase 1 is what shipped. Phases 2 and 3 are still open on the board — the ticket was not marked done because part of it worked.
Nine proof files, each pulled as its own unit of work with a definition of done. No file was started before the previous one compiled clean. When a dependency cycle appeared mid-stream, it surfaced as a concrete blocker rather than a mysterious build failure.
Work spanned many separate sessions with no shared memory between them. Each one resumed from the board: what was proved, what was assumed, which mathlib lemma names had already been checked, and which approaches had already failed and why.
A disproved conjecture, a retracted claim, and every wrong turn are in the log alongside the wins. That record is what stopped the same dead ends being re-explored in a later session — and it is the part most task systems quietly discard.
Generated by the build, not written by hand.
== TXPOF-59 quick build == Build completed successfully (7753 jobs). == Axiom audit == 'TXPOF59.schur_cohn_stable' depends on axioms: [propext, Classical.choice, Quot.sound] 'TXPOF59.ramanujanSum3_eq_zero' depends on axioms: [propext, Classical.choice, Quot.sound] 'TXPOF59.dirichlet_pow4_integral' depends on axioms: [propext, Classical.choice, Quot.sound] 'TXPOF59.jackson_normalized' depends on axioms: [propext, Classical.choice, Quot.sound] 'TXPOF59.jackson_weighted_bound' depends on axioms: [propext, Classical.choice, Quot.sound] 'TXPOF59.RatIvl.hornerIvl_mem' depends on axioms: [propext, Classical.choice, Quot.sound] … 74 more, all identical … == Verdict == No sorries in the build. Axiom audit clean - nothing depends on sorryAx.
The audit runs on every build and inspects all 79 public declarations. It is deliberately not
a grep for the word sorry — a theorem can inherit an admitted lemma through an
import without that word appearing anywhere in its file. #print axioms walks the
entire dependency graph, which is the only check that actually settles the question.
Mathlib has no Fejér kernel, so the hardest lemma had to be built from nothing. Each step below was a separate ticket pull, and each one compiled clean before the next began.
A 2×2 eigenvalue criterion. The first lemma to compile clean, and the first evidence the loop worked.
Character sums over the units of ℤ/3ᵐ vanish for small non-zero frequencies. Hinged on a reindexing lemma that took a full session on its own.
∫₀¹ e(kt) dt = [k = 0]. The foundation everything analytic rests on.
‖gₙ(t)‖² = sin²(nπt)/sin²(πt). Phrased entirely in squared norms, which removes every absolute value and sign case-split.
The integral becomes a finite count of quadruples, then a fibre count, then Gauss-sum arithmetic. An analysis problem turned into combinatorics.
Both targets closed: the Fejér identity ∫₀¹(sin nπt/sin πt)⁴ = n(2n²+1)/3, and the weighted bound ∫ Jₙ(t)|t| ≤ 3/(4n).
Phase 3: kernel-only rational interval arithmetic — sign-aware multiplication, Horner evaluation, and a soundness theorem. No decide, no native_decide: the trusted base does not grow. Mathlib's own interval multiplication explicitly excludes ℚ and ℝ, so this did not exist upstream.
The final bound splits the interval at ±1/(2n). That constant is not cosmetic: it is the minimiser of c²/2 + 1/(32c²), and the four pieces then total exactly n²/2 − 1/4, which clears the target. The obvious choice, 1/n, gives 1.0625n² − 0.25 and fails. It was cheaper to find that out from a numerical check written before the proof than from 200 lines of Lean that could not close.
Including the parts that went badly.
Draft delivered with 5 admitted lemmas and never compiled — the Lean toolchain host was unreachable from the sandbox. Logged explicitly as unverified.
First successful compile, after five corrections to the blind draft. Schur–Cohn clean. The edit → build → read-log loop is established.
Ramanujan reaches zero admitted lemmas. The axiom audit is added to the build script — the previous claim rested only on the absence of warnings.
First audit ever run: 26 declarations, 3 carrying sorryAx. The trust boundary is now measured rather than asserted.
Fejér bridge, counting lemmas, quadruple expansion. Trust boundary unmoved at 3 across four consecutive files — the verified region grows underneath it.
Target (i) closed. Two of the three admitted integrals fall together. 3 → 1.
Three rounds lost to a symptom being treated instead of a cause, and three more to builds run against stale files. Both recorded as process fixes, not just bugs.
62 declarations, 62 clean, zero sorryAx. Phase 1 complete.
Phase 3 lands on the first attempt: certified rational interval arithmetic, 79 declarations, still zero sorryAx. A watcher now rebuilds and re-audits on every save, so the stale-log failure below is structurally impossible.
"The build showed no warnings" is not verification. Put the real check — here,
#print axioms — in the build script so it runs whether or not anyone
remembers to ask, and so its output is an artifact you can hand someone.
Every identity was checked numerically before a line of proof was written. One such check showed the intended split constant would not work — caught in seconds instead of after a day of formalisation.
Phase 1 of three is done, so the ticket stays open. Splitting one gap into five smaller gaps is not progress, and a board that lets you record that plainly is worth more than one that shows green.
A goal reading (a²)⁻¹ = a⁻¹² that ring refuses to close looks
impossible until you notice set left the variable with a body.
clear_value fixes it in one line — but only if someone recorded the cause
rather than the symptom.
Two days later the same board caught two things a write-up would have missed. A recommended
research target was refuted within a day of being logged — and a second lane found
that the goal it was chasing had already been reached, by a ticket filed the day before.
The remaining open link is a single one, (MULT-mass). That is the failure log
earning its keep: specific enough to be checked, so it got checked.
The research program →