Part VI · 1 — Mathematics

draft

The domain closest to "superhuman" — because correctness is verifiable by computer, which enables RL with a perfect reward.

🎨 Figure F-VI.1 — Verified proof. Brief: a theorem being proposed by a neural network (cloud) and checked by a formal verifier (Lean gear) that lights up a "✓ proved" seal. Compendium palette.

Verified proof

1.1 Why mathematics is special

Formal provers (Lean 4 / Coq / Rocq) verify a proof exactly. This gives a perfect reward for RLVR: it generates the proof → the verifier says right/wrong → clean reward. No human-label noise.

1.2 Roadmap for a small team

  1. Install Lean 4 + mathlib4.
  2. Base: DeepSeek-Prover-V1.5 or Qwen2.5-Math-7B.
  3. SFT with mathlib + OpenMathInstruct + DeepSeek-R1 CoTs.
  4. RLVR: generate a candidate proof → check in Lean → reward = passed/did-not-pass

    (GRPO).

  5. Test-time search: beam search + formal verifier.

Realistic resources: 2–4 RTX 4090, 6–12 months, 1 consulting mathematician. It is one of the most accessible "frontier" projects — see the levers in ../05-building-ai/01-frontier-levers.kmd.

1.3 Milestones

AlphaGeometry and AlphaProof (2024) solved olympiad-level mathematics problems by combining a neural network (intuition/proposition) + formal verification — the neuro-symbolic paradigm (ch. 32).