Proving something to a computer means explicitly building the entire world beneath it — not just re-deriving the result.
Why does formalizing the Kepler conjecture cost eleven years of work?
This reads the Kepler question as a way into a deeper puzzle: why is turning an accepted mathematical proof into machine-checkable form so staggeringly expensive — and what does that cost reveal about the gap between reasoning that looks right and reasoning that is verifiably right?
This explores why formalization — rewriting a proof so a computer can check every step — carries a cost that dwarfs the original human proof, and the corpus points to one core answer: you can't formalize a statement, you have to formalize a world. The clearest signal comes from work arguing that autoformalization must move from isolated statements to whole theories Can autoformalization work on individual statements alone?. Even a single theorem sits on a coherent web of axioms, definitions, and lemmas; a human mathematician leans on shared intuition and 'obvious' steps, but a proof assistant demands that every one of those be built explicitly. The eleven years isn't spent re-deriving Kepler — it's spent constructing the missing library beneath it.
That cost is really the price of closing the gap between coherence and validity. RLVR and similar methods can make a reasoning trace locally consistent — each step follows plausibly from the last — without guaranteeing the whole thing is a valid proof Does RLVR actually improve mathematical reasoning or just coherence?. Formalization is the brute-force way of buying validity: instead of trusting that locally coherent steps compose into a globally sound argument, you force a machine to verify the composition. Every gap a human would wave past becomes labor.
There's a deeper reason the labor doesn't compress. Self-improvement in reasoning systems is bounded by a generation–verification gap: producing a candidate is cheap, but reliably confirming it requires something external to validate and enforce What stops large language models from improving themselves?. Formalization is that external verifier made total — which is exactly why it can't be shortcut by cleverness alone. It's also why fully symbolic approaches are so brittle: partial formalization, enriching natural language with selective symbolic structure, often beats full formalization because full symbolic translation loses semantic information and multiplies the pieces that must be reconciled Why does partial formalization outperform full symbolic logic?.
The surprising takeaway the corpus offers is that the bottleneck was never intelligence — it's environmental structure. What makes a domain tractable for automated reasoning is having checkable ground truth, modular pieces, and fast iteration Can small models match frontier reasoning without massive scale?, What makes a research domain suitable for autonomous optimization?. A frontier proof like Kepler's is the opposite: a dense, deeply entangled structure where the 'verifiable' scaffolding has to be laid down by hand before any checking can begin. The eleven years is the time it takes to convert human mathematics — full of trusted shortcuts — into the kind of modular, ground-truthed terrain that a machine can actually walk.
Sources 6 notes
Real formalization requires theory-level work: even one theorem needs a coherent web of axioms, definitions, and lemmas. Statement-level approaches only succeed by borrowing from prebuilt libraries like Mathlib, hiding the actual complexity involved.
RLVR post-training measurably reduces logical errors between adjacent reasoning steps, but locally coherent traces can still be globally invalid proofs. The improvement is structural rather than semantic.
Self-improvement in LLMs is formally bounded by the generation-verification gap, meaning every reliable fix requires something external to validate and enforce it. Models cannot escape this constraint through metacognition alone.
QuaSAR and Logic-of-Thought both achieve 4-8% accuracy gains by enriching natural language with selective symbolic elements rather than replacing it. Full formalization loses semantic information; pure language lacks structure. Augmentation preserves both.
A 3B model trained with curriculum SFT and multi-domain RL reaches 94.3 AIME26 and 80.2 LiveCodeBench scores matching much larger systems. The result is bounded to verifiable tasks with checkable ground truth, where RL can provide clean reward signals.
Show all 6 sources
Autonomous research pipelines require immediate scalar metrics, modular architecture, fast iteration cycles, and version control. Domains lacking any property resist autoresearch regardless of LLM capability, because the bottleneck is environmental structure, not model power.
Papers this line draws on 8
The research behind the notes this line reads — ranked by how closely each paper relates.
- Local Coherence or Global Validity? Investigating RLVR Traces in Math Domains
- Does Reinforcement Learning Really Incentivize Reasoning Capacity in LLMs Beyond the Base Model?
- The Invisible Leash: Why RLVR May Not Escape Its Origin
- Faithful and Robust LLM-Driven Theorem Proving for NLI Explanations
- Large Language Models as Planning Domain Generators
- Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoning
- Theory-Level Autoformalization: From Isolated Statements to Unified Formal Knowledge Bases
- Mind the Gap: Examining the Self-Improvement Capabilities of Large Language Models