One weekend, two open problems: AI agents, exact checks, and Lean make math experiments cheap
Inside account of attacking two open math problems over a weekend with LLM agents, exact-arithmetic programs, and the Lean proof assistant. One problem yielded a machine-checked proof candidate; the other resisted every route. The point: experimentation is getting dramatically cheaper while proof, novelty, and human review stay scarce.