Terence Tao: At the Erdos problem website, AI assistance now becoming routine (mathstodon.xyz)

A recent thread on the Erdös problems site around Problem #367 illustrates a compact human–AI–formal-verification pipeline in action. A human (Wouter van Doorn) posted a disproof of the problem’s second part contingent on a certain congruence identity. Within hours, Gemini Deepthink produced a complete proof of that identity (initially using heavy p-adic algebraic number‑theory), which the poster then distilled by hand into a more elementary argument. Follow-up AI literature searches (Gemini and ChatGPT) turned up related work on consecutive powerful numbers but nothing directly addressing #367. Crucially, the elementary proof was formalized in Lean using the Aristotle tool from Harmonic by Boris Alexeev in 2–3 hours, with the final statement hand-written to guard against possible AI exploits. The episode highlights three technical takeaways for the AI/ML and formal-methods community: (1) state‑of‑the‑art LLMs can rapidly produce nontrivial mathematical proofs (minutes) that may rely on advanced machinery; (2) human experts still play an essential role in simplification, vetting, and choosing presentation; and (3) combining LLM output with interactive theorem provers (and careful hand-formalization of critical statements) makes rigorous verification feasible and practical, pointing toward scalable human–AI workflows for formal mathematics.