AI finally solves some math problems mathematicians couldn't

Mathematicians have long distrusted LLMs because they hallucinate—even confident-sounding wrong answers. These researchers built an agent that uses LLMs to propose proof strategies, then verifies each step in Lean, a proof-checking language that accepts only airtight logic. The system solved 9 previously unsolved Erdős graph problems and proved 44 outstanding OEIS conjectures, at a cost of hundreds of dollars per problem. It's now being used in real research across combinatorics, optimization, and quantum optics, showing AI can genuinely accelerate mathematical discovery when paired with formal verification.