Expensive to Produce, Cheap to Verify
Fundamental asymmetry in formal-verification systems where generating correct proofs requires significant computational and intellectual effort, but verifying their correctness can be done mechanically and efficiently.
Core Asymmetry
Generation Difficulty: Creating lean-proofs requires deep mathematical reasoning, creative insight, and significant computational resources. Current LLMs struggle with direct Lean generation.
Verification Simplicity: Once produced, formal proofs can be checked mechanically by relatively simple verification engines, providing definitive correct/incorrect answers.
Computational Complexity: Reflects fundamental computer science principle where certain problems (like proof search) are computationally hard while verification is comparatively easy.
Implications for AI Training
Training Signal Quality: The verification asymmetry provides clean, binary feedback signals for Reinforcement Learning with Verification - much stronger than statistical approximations.
Scalable Evaluation: Once generated, verified proofs can be checked at scale without human expertise, enabling automated quality assessment.
Resource Allocation: Suggests focusing computational resources on generation capabilities while leveraging efficient verification for training signals.
Economic Model
Production Investment: High upfront costs in developing proof generation capabilities and computational resources.
Verification Efficiency: Low marginal costs for verifying results once generation capabilities exist.
Quality Assurance: Mechanical verification provides reliability guarantees that justify production costs.
Relationship to verified-ai
Business Case: The asymmetry supports axiom-math's approach of investing heavily in proof generation while leveraging cheap verification for training and deployment.
Competitive Moats: Organizations that master expensive generation can create sustainable advantages, as verification alone is insufficient.
Scaling Strategy: Enables systems to generate expensive proofs once and reuse them cheaply across many applications.
Technical Challenges
Generation Bottleneck: Current frontier models still struggle with generating valid formal proofs, creating opportunities for specialized approaches.
Quality vs Speed: Balancing the computational cost of generation against the quality of resulting proofs.
Human-AI Collaboration: May require human insight for complex proof strategies while AI handles mechanical aspects.