收录解读
This paper evaluates LLM-driven formal proof search on open mathematical problems, using Lean-style formal verification as the reliability layer for generated proofs.
The reported system autonomously resolves several open Erdős problems and proves additional OEIS conjectures, showing that formal proof agents can move beyond benchmark exercises into active mathematical research workflows.
The important pattern is not just stronger math reasoning, but a workflow: generation, formal checking, search, cost control, and deployment into real combinatorics and related research contexts.
For this repository, it is a high-value AI-for-math entry because it demonstrates a reusable operating loop for reliable AI-assisted discovery where correctness can be machine-verified.