AI is getting really good at math — we must leverage these capabilities now to make AI safe

AI safety research is facing a critical juncture as mathematical proof-writing AI models approach superhuman capabilities, particularly in formal verification systems like Lean.

Current landscape; Recent developments in AI mathematical reasoning capabilities, exemplified by DeepMind’s AlphaProof achieving IMO Silver Medal performance and o3’s advances in FrontierMath, signal rapid progress in formal mathematical proof generation.

• AlphaProof has demonstrated high-level mathematical reasoning abilities while writing proofs in Lean, a formal verification system
• o3’s breakthrough on the FrontierMath benchmark, combined with advanced coding capabilities, suggests formal proof verification is advancing rapidly
• These developments indicate that superhuman proof-writing capabilities may emerge sooner than previously anticipated

Shifting paradigm; The traditional view that theoretical AI alignment work is more valuable in longer timelines needs reassessment given the accelerating capabilities in formal mathematical reasoning.

• The AI safety community has generally reduced focus on theoretical alignment as development timelines shortened
• Mathematical reasoning capabilities are advancing at a uniquely rapid pace compared to other AI abilities
• Formal verification provides an ideal training environment due to its clean, unambiguous feedback signals

Critical window; A narrow opportunity of 2-3 months exists where advanced mathematical reasoning capabilities could outpace general AI planning abilities.

• This period could allow researchers to leverage near-superhuman mathematical abilities while broader AI capabilities remain limited
• The bottleneck may shift from problem-solving to question-posing skills
• Formal verification will become crucial as models become more sophisticated at obscuring mathematical reasoning flaws

Preparation priorities; Two key actions are recommended for the AI safety research community:

• Establish formal definitions for theoretical AI safety concepts across all relevant fields, without necessarily proving known theorems
• Develop extensive question banks of 100-1000 queries per researcher to maximize efficiency when advanced proof-writing models become available

Looking ahead; The theoretical alignment community faces a pivotal moment where preparation and formal verification tools could significantly impact the field’s ability to leverage upcoming mathematical AI capabilities for safety research.