Erdos problem #728 was solved more or less autonomously by AI
Terence Tao points to a milestone in “AI for math” work: Erdős Problem #728 was reportedly solved with heavy AI assistance after the community clarified what the original (somewhat misformulated) question was trying to ask. Tao’s write-up emphasizes that this was not just a literature lookup or a trivial edge case — it involved iterating on the statement, generating a proof, and then checking and repairing it with formal tooling.
The more interesting takeaway, though, is how quickly the solution was rewritten into different forms. Tao describes a loop where AI produced a proof sketch, a proof assistant workflow (Lean, with help from tools like Aristotle) verified or fixed gaps, and then AI was used again to turn formal proof artifacts into readable exposition. The result isn’t just “a correct proof,” but many versions: short vs. long, narrative vs. technical, and with different levels of background and rigor. That combination — fast rewrite plus formal verification — suggests a future where the limiting factor in sharing math may shift from producing a single polished manuscript to managing a family of tailored explanations.