Who Will Review OpenAI's AI-Generated Math Proofs?

On October 6 (local time), OpenAI caused new controversy when it released 722 research papers containing solutions to math problems created by an unreleased AI model used inside the company.

Usually, other mathematicians check math papers before they are published in academic journals. This process is called "peer review." Even after a paper is published, its authors answer questions and fix mistakes. OpenAI released all its papers at once without this kind of review and did not explain the AI's proofs clearly enough. This has raised questions about who will check hundreds of AI-created proofs and who will be responsible for any mistakes.

OpenAI used a computer tool called "Lean" to check some of the proofs. The tool looks for logical mistakes after solutions are turned into code. However, people still need to check whether the statements in the code match what the original papers say. Passing the computer's logic checks does not mean a proof has been fully reviewed. OpenAI knew its work had raised concerns about review. On September 21, it announced that it had created the "Mathematics and AI Advisory Group, AGMAI," with nine members.

But people still need to read hundreds of papers, find mistakes, and add explanations. Ursula Martin, a professor at Oxford University, criticized OpenAI in Nature, saying, "OpenAI expects the academic community to clean up the messy drafts it has thrown out."

Some people also worry that mathematics as a field may struggle to make use of difficult problems solved by AI. Terence Tao, a professor at the University of California, Los Angeles (UCLA), said, "I feel deep frustration that none of the people involved in these proofs can answer questions or give lectures." Normally, the person who proves a result explains how the solution works, teaches the next generation, and helps other researchers build on the work. That chain of learning and research is now broken.