Formal-Proofs · AI Beat

20 Jul 2026 · AI Beat Desk

An 87-Year Conjecture Falls During the World Cup

Anthropic researcher and mathematician Levent Alpöge used Claude Fable during the World Cup final to produce a concrete, checkable counterexample to the Jacobian Conjecture — a problem on Smale's 1998 list of Mathematical Problems for the Next Century. The map is three polynomials in three variables. The Jacobian determinant is -2. The conjecture is false.

19 Jul 2026 · AI Beat Desk

Thirty Years of Queries

A UC Berkeley IEOR researcher used GPT-5.6 Sol Pro over two chat sessions totaling roughly four hours to prove a lower bound in zeroth-order convex optimization that had resisted attempts for 30 years, then formalized the result in Lean 4. A different kind of AI-does-math story than the CDC proof: one expert, one model, one hard problem.

11 Jul 2026 · AI Beat Desk

Fifty Years, One Hour, Sixty-Four Agents

OpenAI claims GPT-5.6 Sol Ultra produced a three-page proof of the Cycle Double Cover Conjecture — a 50-year-old open problem in graph theory — in under an hour, using 64 parallel subagents. The math community hasn't had a chance to stress-test it yet, and the details of how much human guidance went in are unclear. Worth watching, cautiously.