OpenAI Posts 722 Math Manuscripts From an Unreleased Model

What Happened

On October 6, OpenAI posted a large batch of mathematics research to a public GitHub repository and said it came from an internal frontier model that has not been released. Press coverage puts the haul at 722 manuscripts grouped into 372 families of results, although the repository's own README listed 719 manuscripts when I checked, so "roughly 720" is the safer figure. The announcement is on OpenAI's research page, and the papers live in the openai/math repository.

According to OpenAI, it posed about 4,000 problems to the model, and the average result that survived took roughly three hours of ChatGPT Pro-equivalent compute. The Next Web reports that nearly every paper came from a single prompt to a single AI agent. The repository is licensed under Apache 2.0 and includes Lean formalizations for many of the proofs (the README puts the share of top-line results with a formal version at about 42 percent), plus ten abridged summaries of the model's reasoning.

The titles listed in the repository range widely: the irrationality exponent of pi, the symmetric and general Mahler conjectures, Kaplansky's direct-finiteness conjecture in characteristic two, and a formula for diluted spin glasses. A title on a list is not a settled question, though. OpenAI itself says the results sit at different stages of verification and that some without Lean versions could contain errors, which it promises to fix quickly.

Why It Matters

The first thing that changes is scale. Earlier AI-for-mathematics announcements involved a handful of results at a time; this release spans hundreds of manuscripts across many subfields. If even a fraction of them hold up, the bottleneck in mathematics shifts from producing proofs to understanding, refereeing, and absorbing them. Lean is what makes that shift manageable: a formalized proof is checked by a computer, so the open question becomes whether the theorem was stated correctly and whether anyone grasps why it is true, not whether each step is valid.

The second thing is governance. On September 29, the Advisory Group on Mathematics and AI, hosted by the Institute for Advanced Study, published guidelines asking AI labs to stop testing hard problems on private models and to disclose prompts, time, and compute costs. The group warned that proprietary models could create a two-tier system in the field. OpenAI says it consulted the group and that the repository follows protocols for paper revisions and citations. The group, for its part, has stressed that its advice is not an endorsement of these results or of how they were produced.

The third thing is reproducibility. The Next Web notes that this is the same internal model behind OpenAI's Navier-Stokes claim from September. Because the model is not public, outside researchers cannot rerun it, so the checkable artifacts are the manuscripts and the Lean files, not the process that generated them. That is a real limitation, and it is why so much of the discussion has centered on trust and verification rather than on any single theorem.

Reaction

The Advisory Group's response was measured. It described the release as the beginning, not the completion, of the process of human understanding, according to The Next Web's report. That framing is a reminder that publishing a proof and understanding a proof are different milestones, and that the second one still belongs to people.

Individual mathematicians were more pointed. Tristan Buckmaster of NYU, who had worked on Navier-Stokes before OpenAI's announcement, doubted that so many results could have been carefully checked at once and questioned the due diligence behind the release. Andrew Sutherland of MIT advised treating the single-agent claims as unverified until others can run the model and reproduce the work. OpenAI's Dan Roberts, meanwhile, said that testing internal models helps build better tools and that the proofs were a byproduct of that effort.

What stands out in the coverage I reviewed is that the disagreement is mostly about process: how results were verified, who gets credit, and who gets access to the model. I did not find reporting that identifies a specific broken proof in this batch, and none of the results has gone through independent peer review yet, so it is too early to say how many will stand.

What's Next

OpenAI says it will add Lean formalizations as they become available, keep earlier versions of every paper public, and fund workshops, conferences, and special programs on understanding AI-produced results, with details still to come. The GitHub repository is described as a temporary venue, and the company says it is exploring community-hosted options that meet the Advisory Group's guidelines. It also says it is working to release the model responsibly, but it has not given a date.

Two items in the repository did not follow the standard production procedure, according to its README: a zero-free region for the Riemann zeta function, whose write-up was edited by humans for readability, and a proof of the Hodge conjecture for CM abelian varieties. The diagram above illustrates the underlying idea of the Hodge conjecture, in which a topological cycle is matched to the zero set of an algebraic subvariety. Claims in areas this central will draw the closest scrutiny, and they should be read as claims until independent experts weigh in.

For readers following along, the practical checkpoints are straightforward: how much of the repository gets a Lean formalization, whether outside groups can confirm or break specific results, and whether the model eventually becomes available for others to test.

Closing Thoughts

Mathematics is unusual among research fields because its claims can, in principle, be checked to the last step. That is what makes this release interesting rather than merely loud. A pile of proofs that arrives faster than anyone can read it is a new kind of problem, and the field's response, with formal verification, shared guidelines, and public repositories, will probably matter more than any individual result in the batch.

The image above shows the Riemann zeta function plotted in the complex plane using domain coloring. A zero-free region is a statement about where the function's zeros cannot lie, which is the kind of result that bears on how primes are distributed. Whether the version in this repository holds up is exactly what the community now has to determine.

The useful posture, for now, is neither awe nor dismissal. Treat the manuscripts as a large set of well-organized claims, watch which ones get formalized and independently confirmed, and notice how the norms around disclosure and credit evolve as labs keep pointing powerful models at open problems.

한글 요약

OpenAI는 10월 6일 아직 공개하지 않은 내부 최신 모델이 만들었다는 수학 연구 결과를 GitHub 저장소에 대거 공개했습니다. 보도에 따르면 원고는 722편, 결과 묶음은 372개이며, 저장소 README에는 719편으로 적혀 있어 대략 720편 안팎으로 보는 것이 안전합니다. 약 4,000개 문제를 모델에 던졌고 결과 하나당 평균 ChatGPT Pro 기준 약 3시간의 연산이 쓰였다고 OpenAI는 밝혔습니다. 상당수 증명에는 컴퓨터가 검증하는 Lean 형식화가 붙어 있지만(README 기준 주요 결과의 약 42%), 형식화되지 않은 결과에는 오류가 있을 수 있다고 OpenAI도 인정했습니다.

이번 공개의 의미는 규모와 검증 문제에 있습니다. 수학의 병목이 증명을 만드는 일에서 증명을 이해하고 검토하는 일로 옮겨갈 수 있기 때문입니다. 프린스턴 고등연구소가 지원하는 수학·AI 자문그룹은 9월 29일 비공개 모델로 난제를 시험하지 말고 프롬프트와 연산 비용을 공개하라는 지침을 냈고, 이번 결과를 보증하는 것은 아니라고 선을 그었습니다. 뉴욕대 트리스탄 벅마스터는 이 많은 결과를 충분히 검증했는지 의문을 제기했고, MIT의 앤드루 서덜랜드는 다른 연구자가 모델을 돌려 재현하기 전까지는 검증되지 않은 주장으로 다뤄야 한다고 조언했습니다.

앞으로 OpenAI는 형식화를 추가하고 문제 있는 결과를 빠르게 고치며, AI가 만든 결과를 이해하기 위한 워크숍과 프로그램을 지원하겠다고 했습니다. 모델 공개 시점은 아직 정해지지 않았습니다. 지금으로서는 이 원고들을 잘 정리된 대규모 주장으로 보고, 어떤 결과가 형식화되고 외부에서 확인되는지 지켜보는 태도가 적절합니다. 참고: OpenAI 연구 페이지, GitHub openai/math 저장소, The Next Web 보도.