Colin Powers, Ahmed Al Fardan, and Kenzo Yamaguchi
On October 6th, OpenAI published a public repository of roughly 720 manuscripts, generated by an unreleased internal AI model and purporting to solve a range of high-profile mathematics problems. Some of those problems come with formal proofs written in Lean, a programming language that lets a computer check every step within a proof based on many fundamental theorems and lemmas in its database. OpenAI’s announcement and the repository’s README describe maps the model’s entire process step-by-step. OpenAI states that they “want this progress to push the frontier of human knowledge and enable further progress in mathematics.” The very next day, the Association for Human Mathematics (AHM) published a statement saying that mathematicians “did not ask for this work to be done,” and calling for other mathematicians to stop working with OpenAI. We chose this story because it raises a question we face as fellow undergraduate students studying Mathematics, Economics, and Data Science: if a computer can confirm that a statement is true but no human can yet explain why, what have we actually learned? We are interested in what counts as understanding and process in mathematics, and what it means for our fields.
It is fair to say that the recent accomplishments AI has made in Mathematics have created a frenzy within the community, which was already on the edge. A doctoral student shared with Quanta that the constant stream of AI proofs humans don’t yet understand, “breaks our system.” WIRED reported that several OpenAI employees believe their technology has already made mathematics a “dead field.” On the other hand, some mathematicians welcome the release of mathematical proof as something good for the community. Jeremy Avigad from Carnegie Mellon argued that publishing results fits mathematics’ open culture, while Terence Tao has described the moment as an opportunity for mathematicians to clarify why they do math in the first place. Beneath both reactions is a question that has little to do with whether the results are correct, but the inquiry rests on the question, what is a proof for?
This question impacts our understanding of mathematics and its process. To see what these advancements mean, we took a look at Family 159 in OpenAI’s repository, which covers the Erdős reciprocal-sum conjecture and quasipolynomial Szemerédi bounds, an area of combinatorics adjacent to the research that we are involved with on campus. We study the polynomial method, including polynomial partitioning and the Erdős distinct distances problem. We could follow the statement and why the claimed result is interesting, but the proof made absolutely no sense to us. For example, the argument builds polynomial cells in a hierarchy of decreasing dimensions and precision. Even though we work with polynomials in our own research, we could not see why each step was needed.
The day before the release of proofs, Quanta reported that AI-generated proofs are currently almost impossible to read, and that mathematicians know that the machine-checked proofs are true, however they remain unaware of the process. As undergraduate students, whose majors entail heavy focus on mathematics, in our coursework and research, confirming that a result is true is only a part of the process. The challenging part is in understanding the process result well enough to apply it to another problem. This means that a proof we can’t follow can’t teach us anything yet.
Grant Sanderson, creator of 3Blue1Brown and also known for explaining mathematics visually, argues in a video, released on October 16th, that proof has long served as a stand-in for understanding, and that machine-generated proofs should now be treated as raw data for building theory, not as the goal (23:36). In our own research, the matches we found with Family 159, the proof was on the page, but without the understanding of the process behind it, our understanding of the proof remained unsuccessful. Sanderson adds that the machine “can’t understand it for you” (24:58), and he compares doing proofs manually to lifting weights: machines can lift more, but the value comes from doing the repetitions and motions of lifting (16:16). As undergraduates, that is how we approach proofs we see in our coursework, because most of what we are studying in coursework already has a known solution, but building problem-solving skills is what matters. Sanderson expects today’s unreadable proofs to be a temporary problem, since AI companies have every reason and methods to make their models explain themselves better (21:45). He may be right. But even a clearer explanation would still have to be checked manually, and that raises the question of what has been verified so far in terms of AI proofs.
So what has been verified? We believe it’s less than what the headlines suggest. OpenAI’s own README says not every manuscript has a Lean formalization and warns that some unformalized results could have issues. OpenAI has already withdrawn three manuscripts. Even for Family 159, OpenAI’s Lean documentation says the formalization covers the reciprocal-sum consequence and not the paper’s quantitative bound. Additionally, a Lean check only confirms that a proof matches its formal statement, but not that the statement captures the problem, which mathematicians care about.
Where does this lead us? We don’t think the answer is to ignore these results, but we think that releasing them in bulk is not enough. The Leiden Declaration, endorsed by the International Mathematical Union, recommends disclosing AI use, keeping results independently verifiable, and leaving responsibility for correctness with human authors. In our opinion, labs should release explanations with proofs and have outside mathematicians check claims before announcing them. Universities should rethink how mathematical processes are taught and measured, and, as Sanderson suggests, students’ ability to explain proofs aloud will matter more (39:24). For students, the lesson is to keep doing the proofs ourselves. If you study math, pick a result from OpenAI’s repository in an area you are familiar with and try to explain the result to someone else. Getting stuck along the way shows how far a verified result can be from truly understood one.
Course Instructor: Dr. Ainehi Edoro
Associate Professor, Dept. of English
email: aedoro@wisc.edu
Editor: Shrinjita Biswas
PhD Candidate, Interdisciplinary Theatre Studies
Works Cited:
Association for Human Mathematics. “AHM Statement on OpenAI’s October 6 Release of Mathematical Documents.” What’s New (Terence Tao’s blog), 7 Oct. 2026. https://terrytao.wordpress.com/2026/10/07/ahm-statement-on-openais-october-6-release-of-mathematical-documents
Cepelewicz, Jordana. “Is AI the End of Math As We Know It?” Quanta Magazine, 5 Oct. 2026. https://quantamagazine.org/is-ai-the-end-of-math-as-we-know-it-20261005
Kakaes, Konstantin. “Deluge of 377 OpenAI Proofs Bewilders the Math World.” Quanta Magazine, Oct. 2026. https://www.quantamagazine.org/update/167703/
Leiden Declaration on Artificial Intelligence and Mathematics. 2 June 2026. https://leidendeclaration.ai/
OpenAI. “Family 159: Lean Formalization Scope.” GitHub, openai/math. https://github.com/openai/math/blob/main/lean/docs/159.md
OpenAI. “history.md.” GitHub, openai/math. https://github.com/openai/math/blob/main/history.md
OpenAI. “openai/math.” GitHub, 6 Oct. 2026. https://github.com/openai/math
OpenAI. “Sharing AI Progress in Mathematics.” OpenAI, 6 Oct. 2026. https://openai.com/index/sharing-ai-progress-in-mathematics/
Sanderson, Grant. “There’s Never Been a Better Time to Go into Math.” YouTube, uploaded by 3Blue1Brown, 16 Oct. 2026. https://www.youtube.com/watch?v=LKrwhjOI8Nc
Scientific American. “Mathematicians Confront the AI Apocalypse.” https://scientificamerican.com/article/mathematicians-confront-the-ai-apocalypse
Ward, Isabella. “OpenAI Is Pissing Off a Bunch of Mathematicians-Again.” WIRED, 6 Oct. 2026. https://www.wired.com/story/openai-is-pissing-off-a-bunch-of-mathematicians-again/
Image: Casey Reas, There’s No Distance 2.1 (2021), video still, via Sotheby’s
