AI-Assisted Proof and Formalization of Erdős Problem #367 on Mathstodon

In a recent development in the world of mathematical research, the Mastodon server mathstodon.xyz has become a hub for collaborative problem-solving, particularly with the help of AI. A notable example is the resolution of Erdős problem #367, which showcases how AI tools can complement human intuition and formal verification methods.

The Problem and Initial Disproof

Erdős problem #367, listed on the Erdős Problems website, was recently tackled by Wouter van Doorn. On November 20, Van Doorn proposed a disproof of the second part of the problem, contingent on a specific congruence identity he believed to be true. He confidently stated that "someone here is able to verify... does indeed hold."

AI Verification and Proof Refinement

A few hours later, Terence Tao, a renowned mathematician, posed Van Doorn's proposed identity to Gemini Deepthink, an advanced AI model from Google. After approximately ten minutes, Gemini produced a complete proof of the identity using p-adic algebraic number theory-a somewhat overkill approach for this problem.

Tao then manually converted the AI-generated proof into a more elementary form, which he presented on the Erdős Problems website. He noted that the resulting proof was suitable for "vibe formalizing" in Lean, a popular theorem prover used in formal verification.

Formalization with Lean

Two days later, Boris Alexeev took up the task of formalizing Tao's refined proof using the Aristotle tool from Harmonic. This process involved translating the proof into Lean code while ensuring that the final statement was verified by hand to prevent any potential AI exploits. The entire formalization process took between two to three hours, and the resulting Lean file is available at Boris Alexeev's website.

Additional Literature Search

To round out the project, Tao conducted an AI-assisted literature search on the problem using ChatGPT and Gemini. After about fifteen minutes, these tools turned up some related literature on consecutive powerful numbers but found no direct connections to Erdős problem #367. The detailed results of this literature search can be found at ChatGPT's share link and Gemini's share link.

Implications for Mathematical Research

This case study highlights the growing role of AI in mathematical research. Here are a few key takeaways:

• AI as a Proof Assistant: Advanced models like Gemini Deepthink can generate complex proofs, even if they sometimes use overkill methods. This capability can significantly speed up the initial stages of problem-solving.
• Human-AI Collaboration: The process of refining AI-generated proofs into more elementary forms and then formalizing them in Lean demonstrates the importance of human oversight and expertise in ensuring correctness and clarity.
• Formal Verification: Tools like Lean are essential for formally verifying mathematical statements, providing a high level of confidence in the results. This is particularly important in areas where subtle errors can have significant implications.

Conclusion

The resolution of Erdős problem #367 on mathstodon.xyz is a prime example of how AI and human collaboration can accelerate mathematical research. By leveraging AI for initial proofs and formal verification, researchers can focus more on creative problem-solving and less on tedious verification tasks. This synergy between AI and human expertise promises to open new avenues in the field of mathematics.