The subject matter falls under the intersection of Computational Mathematics, Automated Theorem Proving (ATP), and Formal Verification.
A suitable review body for this topic would be Computational Mathematicians and Formal Verification Experts.
Abstract
This analysis details the recent application of advanced AI tools, including large language models (LLMs) and formal proof assistants (Lean, Aristotle), to solve Erdős Problem #728, a question concerning the prime factorization of binomial coefficients originally posed in 1975. While the autonomous solution of the problem is a significant milestone—particularly because the problem required reconstruction due to initial misformulation—the primary takeaway is the demonstrated capability of AI to rapidly generate, revise, and formalize the exposition of the mathematical proof. This "high-multiplicity" revision capability contrasts sharply with traditional, time-consuming human manuscript production, suggesting a future paradigm where a single core argument can generate multiple tailored, formally verified, and narrative-structured articles for different levels of rigor and audiences.
Summary: AI Capabilities in Mathematical Proof Generation and Exposition
AI Solves an Erdős Problem: The application of AI tools successfully solved Erdős Problem #728, concerning the divisibility condition $a!b! | n!(a+b-n)!$ subject to constraints $a, b \ge \epsilon n$ and $a+b > n + C \log n$.
Problem Reconstruction (2d): The original 1975 problem, posed by Erdős, Graham, Ruzsa, and Strauss, was vaguely worded. Trivial solutions were identified by an AlphaProof-associated team, necessitating the community-imposed constraint $a,b \le (1-\epsilon)n$ to adhere to the intended spirit of the question.
Initial Solution and Formalization (Jan 4): ChatGPT produced a proof for the adjusted constraint, but only for a small constant $C$. This proof was subsequently formalized by the AI tool Aristotle into Lean code, highlighting a fast transition from heuristic LLM output to machine-verifiable proof.
Iterative Exposition Improvement (3/5): Following the initial solution, the Lean proof was run through ChatGPT to generate a natural language exposition. Subsequent conversational prompting yielded an improved write-up that filled gaps in the original proof, though the style remained "clunky" and "AI"-like.
Achieving the Target Result (4/5): Further prompting enabled ChatGPT to adapt the argument to solve the version of the problem intended by Erdős (handling large $C$). This proof contained minor errors that were automatically repaired by the formal proof assistant Aristotle, resulting in a Lean-verified proof of a result new to the literature.
Rapid Manuscript Generation (4/5): A third participant created a shorter Lean proof via Aristotle, which was then subjected to a lengthy back-and-forth ChatGPT session. This process generated a "fully fleshed article" describing the proof, its connection to prior literature, and exhibiting an acceptable narrative structure for a research paper standard.
Core Revelation: Dynamic Rewriting (5/5): The key capability demonstrated is the ability of AI to rapidly write and globally rewrite expositions of complex proofs, irrespective of the original author. This contrasts with traditional mathematical practice where major revisions are avoided due to required effort and the risk of introducing new errors.
Future Publishing Model (5/5): The combination of competent AI text generation and formal proof verification (via Lean) allows for a dynamic and high-multiplicity concept of argument write-up. While a human-generated "official" paper remains preferred, it could be accompanied by multiple AI-generated secondary versions tailored for different levels of rigor, thus adding value beyond the primary artifact.
Significance Assessment (2m):* The result of solving Erdős Problem #728 is deemed by the expert not publishable by itself but suitable for inclusion in a larger paper surveying the state of related binomial coefficient divisibility problems. The AI's role is seen as systematically exploring the application of well-understood methods across large problem classes at an impracticable scale for human mathematicians.