Towards Solving More Challenging IMO Problems via Decoupled Reasoning and Proving

Zhenwen Liang, Linfeng Song, Yang Li +4

Automated Theorem Proving (ATP) in formal languages is a foundational challenge for AI. While Large Language Models (LLMs) have driven remarkable progress, a significant gap remain…