Recently, the application of AI tools to Erdos problems passed a milestone: an Erdos problem (#728 https://www.erdosproblems.com/728) was solved more or less autonomously by AI (after some feedback from an initial attempt), in the spirit of the problem (as reconstructed by the Erdos problem website community), with the result (to the best of our knowledge) not replicated in existing literature (although similar results proven by similar methods were located).

This is a demonstration of the genuine increase in capability of these tools in recent months, and is largely consistent with other recent demonstrations of AI using existing methods to resolve Erdos problems, although in most previous cases a solution to these problems was later located in the literature, as discussed in https://mathstodon.xyz/deck/@tao/115788262274999408 .  This particular case was unusual in that the problem as stated by Erdos was misformulated, with a reconstruction of the problem in the intended spirit only obtained in the last few months, which helps explain the lack of prior literature on the problem.  However, I would like to talk here about another aspect of the story which I find more interesting than the solution itself, which is the emerging AI-powered capability to rapidly write and rewrite expositions of the solution.  (1/5)

Hacker News is a community-driven platform for sharing and discussing technology news, startups, and programming-related topics. Through user submissions and comments, Hacker News offers insights into emerging technology trends, industry developments, and entrepreneurial ventures. Readers can participate in discussions, share their insights, and stay informed about the latest advancements in technology and innovation.

Hacker News

AI tools autonomously solved an Erdős problem (#728) for the first time, marking a milestone in mathematical AI capabilities. Beyond the solution itself, the more significant development is AI's ability to rapidly generate and rewrite mathematical proofs in multiple formats—from formal Lean code to natural language expositions. This enables dynamic, multi-version documentation where AI can produce tailored writeups at different rigor levels, verified by proof assistants. The workflow involved ChatGPT generating proofs, Aristotle formalizing them in Lean, and iterative refinement through human feedback, ultimately producing publication-quality mathematical writing.

Terence Tao: "Recently, the application of A…"