Open Problems Solved by LLMs? A Survey of Verifiable Mathematical Discovery [pdf] (aclanthology.org)

A new survey titled "Open Problems Solved by LLMs?" presents a comprehensive analysis of how Large Language Models (LLMs) contribute to addressing previously "open" mathematical problems. Researchers Ioannis Tzachristas, Georgios Tzachristas, and Aifen Sui argue that while claims of LLMs solving open problems are thrilling, they can be misleading. The paper emphasizes that successful results typically rely on closed-loop discovery systems rather than one-time proof generation, incorporating mechanisms where LLMs function as proposal generators evaluated by external verifiers. Key design patterns and techniques, including the use of formal proofs, search mechanisms, and verification frameworks, are outlined as essential for achieving verifiable mathematical discoveries. This work is significant for the AI/ML community as it establishes an evidence ladder to assess claims of mathematical solutions produced by LLMs, promoting accountability and reproducibility in this emerging field. By categorizing the complexity of mathematical tasks and identifying which areas present the greatest challenges for LLMs, the survey aims to guide future research and system designs. Ultimately, the researchers advocate for understanding generative models as reliable tools for mathematical discovery, stressing the importance of independent verification to build trust and enable further advancements in AI-driven scientific inquiry.