Why Does the Debate Between Mathematicians and OpenAI Remind Me of Software Engineering?
From coding agents to AI-generated mathematical proofs, stronger generation capabilities are changing professional work. Correctness needs new verification and collaboration mechanisms; value depends on problems, theories, and accumulated knowledge.
On October 6, 2026, OpenAI published mathematical research manuscripts and claimed results generated by an internal model on GitHub. The debate surrounding these materials reminded me of the discussions when coding agents first entered software development.
Will AI skip essential steps in a derivation? Can its results be trusted? If only the generator knows what it meant, how can others check and use the work? These questions are familiar to software developers.
Mathematicians’ concerns also reach further. In its subsequent statement, the Association for Human Mathematics (AHM) emphasized human understanding as a purpose of mathematical research. Earlier recommendations from the Advisory Group on Mathematics and Artificial Intelligence also made helping the community understand and assimilate results an important responsibility of publication.
As a software developer, I strongly relate to one question: do we need more output, or more work worth using and studying further?
Following the changes brought by coding agents, I see three connected questions in this debate: how machines participate in production, how correctness is assured, and what is worth producing.
How software engineering began accepting coding agents
Early AI-generated code frequently fabricated APIs, missed edge cases, or ran without correctly implementing requirements. Developers still need to deal with these problems today.
Meanwhile, more teams have incorporated agents into actual workflows. Specifications clarify tasks, automated tests and static analysis provide feedback, continuous integration (CI) checks changes, and code review helps teams assess implementation and design.
These arrangements make errors easier to discover, contain, and correct. Improving model capabilities also matters, but reliable collaboration requires organizing requirements and feedback.
I find this more useful than requiring an agent to reproduce a particular programmer’s thought process. Different implementation paths can be checked against the same behavioral requirements and engineering standards. People still need to understand key designs, while judgments about usability increasingly rely on independent verification.
When AI-generated mathematical proofs raise reliability problems, I therefore first ask which requirements can be made clearer, which errors independent checks can detect, and which feedback can improve the next attempt.
AI making mistakes is a starting point for designing verification systems. Specific errors also give us concrete targets for improving those systems.
Mathematics already has stronger verification tools
Lean is both a programming language and a proof assistant. Using it means expressing mathematical objects, statements, and proofs in a form a computer can process. A small logical kernel then checks whether a complete proof establishes its conclusion from the declared assumptions.
For example, to prove that every natural number n satisfies n + 0 = n, ordinary tests can substitute many numbers and check those cases. A formal proof instead needs a derivation that applies to any n, using definitions or established theorems. Lean checks that derivation.
A person or an AI system can write the proof. Its checking mechanism is independent of the generator and of another model’s score. Subject to its logic, axioms, and the trustworthiness of the checker, it offers guarantees about formal statements that ordinary software tests cannot.
Another task is checking whether the formal statement expresses the original problem. Suppose the original concerns all integers but the formal version considers only positive integers. Even if the proof passes checks, its scope has narrowed.
This error can become a concrete target for checking: compare the domains in the original text and formal declaration, include zero and negative numbers in sample checks, and examine whether added assumptions change the problem. Sample checks can expose some mismatches; reviewing the declaration directly examines what is being proved. Tools can assist both, and independent review can be arranged.
This corresponds to two activities in software engineering: verification, checking that work follows the specification, and validation, checking that the specification expresses the actual goal. Recording the object, method, and results of each check helps locate problems and identify improvements for the next round.
This is the direction I value: when reliability problems arise, keep looking for checks and feedback that can be performed independently. Formal mathematics offers strong foundations, while expressing statements and aligning their meaning also deserve further engineering work.
Mathlib’s review bottleneck is a concrete example
Mathlib is an open-source library of formal mathematics built on Lean. The Mathlib Initiative’s October 2026–March 2027 roadmap reports more than two million lines of formal mathematics and over 750 contributors.
The roadmap identifies review capacity as the principal constraint on growth: review throughput increased over the previous year, yet the open pull request queue continued growing. The Initiative plans to maintain a baseline of roughly 130 review rounds per week, expand the reviewer pool, turn recurring feedback into automated checks, and improve tools that show changes to Lean declarations.
These are familiar software engineering measures. Generation, checking, and integration into shared knowledge each have their own processing capacity and need to improve together.
Formal Frontier’s project description explains why review remains necessary after proof checks pass: artifacts can duplicate existing material, introduce poor definitions, ignore established APIs, or leave proofs that are difficult to maintain. These problems affect whether knowledge can be reused.
The May 2026 preprint MathlibPR: Pull Request Merge-Readiness Benchmark for Formal Mathematical Libraries studies this layer of judgment too. Its abstract reports that the evaluated models and agents struggled to distinguish merge-ready PRs from PRs that passed builds but still required revisions or were never merged.
Mathlib’s existing backlog arises from expanding collaboration. The roadmap also anticipates greater AI assistance in downstream projects. This shows me that the formal mathematics community is already adjusting verification, review, and collaboration mechanisms to accommodate changing production methods.
After verification, what is worth producing?
Even if checking and review become more efficient, a question remains: why do this work?
Coding agents have reduced the cost of many implementations. Yet different people and teams using similar tools still produce very different software.
The difference comes from problem selection, understanding requirements, system design, and tradeoffs. One team may implement many features faster without resolving what users actually need. Another may make only a few key changes and noticeably improve the experience.
Tests can establish that behavior meets requirements. Whether those requirements deserve investment, and what value implementing them creates, require judgment in the context of actual use.
Mathematical research faces a similar question. A proof can be correct and a result new, while its contribution to knowledge also depends on whether it reveals structures, connects previously separate areas, poses valuable questions, or provides a clearer explanation for a collection of existing results.
At least part of mathematicians’ emphasis on understanding concerns this capacity for further research. After understanding a result, can others apply it to new problems? Can a group of proofs become an explanatory theory? These questions determine how knowledge continues growing.
I therefore favor treating proof counts as one measure of output and including the development of understanding, connections, and subsequent research in evaluating results. When generating a class of proofs becomes cheaper, these activities deserve more investment.
AI can participate in problem definition, abstraction, verification, and judgments of value too. Future divisions of work may continue changing; evaluation still needs to consider what the results actually add.
Reconsidering the debate
Returning to OpenAI’s release, its announcement describes some Lean formalizations, revision and citation arrangements, and plans to support subsequent understanding. What should be observed next is whether these arrangements help researchers independently verify, understand, and use the results.
Batch generation increases the material the community needs to process. Those generating it should bear corresponding responsibilities for verification, organization, and support. This is work needed for new production capabilities to enter professional collaboration.
At the same time, I think quality requirements and specific working habits can be examined separately. Machines can explore differently from people, while professional communities need methods for checking those results, organizing collaboration, and accumulating knowledge.
Software engineering is experiencing this change. As agents take on more implementation, specifications, tests, review, and system design need to adjust. Teams still need to decide which requirements deserve implementation. The practices of the formal mathematics community show similar adjustments taking place.
For AI mathematical research, I hope to see more reliable independent proof checks, easier comparison of statements, automated handling of recurring review issues, and researchers developing new understanding and connections from generated results.
This moves evaluation from how much was generated toward how results hold, how they are used, and how they help knowledge grow.
As AI lowers production costs, the priorities of professional work shift: ensure correctness, organize effective collaboration, and judge what is worth producing.
I think the debate between OpenAI and mathematicians deserves continued discussion because it brings all three activities into view. As the ability to generate code and proofs increases, the value of software and mathematics still takes shape through concrete problems, design, and accumulated knowledge.