The Data Exchange with Ben Lorica Building Mathematical Superintelligence
27 snips
Apr 16, 2026 
Tudor Achim, cofounder of Harmonic and computer scientist building AI for formalized mathematics. He defines mathematical superintelligence and contrasts search with pattern recognition. He reviews rapid AI progress on IMO-level math and describes hybrid systems that pair neural methods with formal provers like Lean. He outlines interfaces, workflows, and applications beyond pure math.
AI Snips
Chapters
Transcript
Episode notes
IMO Gold Claims Show Rapid Progress
- At the 2025 IMO several groups claimed gold medal performance using different approaches: OpenAI and DeepMind with informal reasoning, Harmonic with formal reasoning, and later ByteDance's prover.
- Achim published a tech report on Harmonic's formal system that reached IMO-level performance within months.
Hybrid Systems Are Effective But Not Final
- Harmonic's system is hybrid: a fuzzy informal-reasoning component plus a formal prover, and the interplay produced search traces that solved problems.
- Achim warns architectures will evolve quickly and hybrid designs are a snapshot, not a final blueprint.
Prefer Formal Proofs In Lean For Reliability
- Use formal theorem provers like Lean to get airtight, hallucination-free verification because Lean compiles proofs into a machine-checkable form.
- Harmonic chose Lean to make AI-produced proofs human-navigable and to give a strong RL reward signal via compilation.