Researchers introduce Enumerate-Conjecture-Prove (ECP), a neuro-symbolic framework that combines general LLMs and prover LLMs to formally solve mathematical answer-construction problems in Lean. The approach addresses a critical gap where current AI systems struggle with generating both candidate answers and rigorous formal proofs, achieving higher success rates than baseline LLM approaches on competition mathematics benchmarks.
The paper tackles a fundamental asymmetry in how current AI systems approach formal mathematics. While theorem-proving—proving an already-stated proposition—has benefited significantly from advances in LLMs and formal verification tools, answer-construction problems remain underexplored. These problems require not just logical reasoning but creative object generation followed by rigorous verification, a two-stage process that neither general-purpose LLMs nor specialized prover models excel at independently.
ECP's hybrid architecture reflects a pragmatic understanding of AI capabilities. General LLMs possess stronger intuition and reasoning for mathematical exploration but are unreliable at formal proof generation, making them expensive to deploy at scale. Prover-specialized LLMs solve the proof verification bottleneck efficiently but lack the mathematical reasoning needed to propose correct candidate answers. By orchestrating these systems sequentially—using general LLMs for conjecture and enumeration, then prover LLMs for verification—ECP sidesteps both limitations.
The framework's emphasis on canonical answers rather than circular proofs addresses a subtle but critical issue in automated mathematics. Proof checkers like Lean can verify logical correctness without ensuring that a solution meets competition standards, potentially accepting trivial or self-referential witnesses. ECP's integration of admissibility constraints guards against this.
Results on PutnamBench and MathArena demonstrate meaningful but modest progress, solving 17-24% of instances. This reflects the genuine difficulty of the problem class. For the AI and formal mathematics communities, ECP's success signals that hybrid neuro-symbolic approaches may be more effective than single-model scaling for complex reasoning tasks requiring both creativity and rigor.
- →ECP combines general LLMs for mathematical reasoning with specialized prover LLMs for formal verification, addressing complementary weaknesses in current AI systems.
- →The framework enforces canonical answer requirements, preventing Lean proof checkers from accepting circular or trivial solutions that pass syntactic verification.
- →Success rates of 17-24% on mathematical competition benchmarks exceed single-model baselines at equivalent computational budgets.
- →Hybrid neuro-symbolic approaches may outperform scaling single models for tasks requiring both creative reasoning and formal rigor.
- →The research advances formal mathematics automation in domains beyond theorem-proving, targeting the less-studied answer-construction problem class.