Over 700 AI-generated math manuscripts from OpenAI prompt worries about verifying proofs

A bulk release of machine-written mathematics

On October 6, OpenAI released more than seven hundred mathematical manuscripts produced by an internal AI system, according to theoretical computer scientist Nisheeth Vishnoi. In an essay titled "Who Taught the Machines Mathematics?" that reached the Hacker News front page, Vishnoi reports that some of the manuscripts come with formal proofs in the Lean proof assistant, while others are at earlier stages of verification. He writes that OpenAI has acknowledged some of the results may contain errors and has invited the community to examine them.

For a sense of scale, Vishnoi compares the drop to chairing the FOCS program committee in 2021, when roughly four hundred submissions arrived over a couple of days. That flood felt like the yearly output of a community he knew; this release, he writes, produced a sense of distance he could not get past, and he ended up reading very little of it.

Trust conventions built for individual claims

The essay's core observation is that mathematics polices itself through personal stake. A mathematician who announces a result ties their reputation to it, is expected to have spent months or years understanding the argument before going public, and can pay for a serious error for years afterward. Vishnoi notes that even the best mathematicians, himself included, have published incorrect proofs.

A corporate bulk release inverts that structure. Attention accrues from the sheer number of results, while the cost of any single mistake is spread thin across the batch. Vishnoi is not sure the conventions through which mathematics has maintained trust were designed for results produced and announced this way.

Checking is the expensive part

Understanding one unfamiliar proof, Vishnoi writes, can take a mathematician days or weeks: working through the details, checking that the statement captures the original problem, and comparing against what is already known. Formal proof systems help considerably, but deciding which results matter is a separate question, one of taste, and he notes that a machine trained to recognize mathematical taste was not part of what OpenAI presented.

The result is an asymmetry. The company can generate manuscripts relatively cheaply, while the attention needed to make sense of them does not materialize just because they were published. Vishnoi connects this to an essay he wrote in May, "The Branch and the Wish," in which he worried that verification is a skill learned through years of apprenticeship and could erode if mathematics is increasingly delegated to machines. The new release adds a second possibility: the existing capacity for verification may simply be swamped by the quantity of material.

Where the machines' mathematics came from

Vishnoi's own areas, including the Unique Games Conjecture, sparsest cut, graph Laplacians and optimization, appear in the release, and he says OpenAI claims to have resolved some problems he spent years on. He reflects on the time spent training students and walking colleagues through results, passing on knowledge that rarely reaches print: why a particular reduction is useful, why a natural approach will fail, how to tell when a problem is badly formulated. Much of it lived in conversations and on blackboards rather than in papers.

Many mathematicians trained at universities, including people he taught and worked with, have moved into AI companies. Vishnoi stresses that he has no objection to that movement, and notes that older industrial laboratories were open participants in their fields. His concern is the shape of the exchange: universities train people with public support and in a culture meant to share knowledge, companies then gather expertise built over generations and turn it into proprietary systems backed by computing resources universities cannot match, and the people who developed that knowledge have little say in what gets built from it.

Why it matters

For formal verification, the release is a practical landmark rather than a curiosity: hundreds of machine-produced mathematical results, a subset carrying Lean proofs, move machine-checked mathematics toward bulk production, where correctness no longer depends on the reputation of an author. Vishnoi's essay argues that the human systems around that output, from review capacity to prioritization to how credit and blame are assigned, scale badly against cheap generation. If releases like this become routine, the field's bottleneck shifts from producing proofs to deciding which ones deserve scarce human attention. The essay also frames a broader question for research institutions: when publicly developed knowledge becomes proprietary capability, the traditional exchange between universities and industry stops working the way both sides assumed.