OpenAI withdraws three demonstrations after one day and calls the ‘mathematical pact’ into question

On Tuesday 6 October, an OpenAI repository, simply named ‘math’, appeared on GitHub. It contains 722 mathematical papers organised into 372 families of results, ranging from algebraic geometry to theoretical computer science, all generated by an in-house model that the company has not released and whose name it has refused to disclose. Less than twenty-four hours later, three of those papers had already been retracted due to an error – a reversal of roles that is highly unusual in the history of scientific retractions, where it is usually a single researcher facing accusations who has to backtrack, and almost never one of the world’s leading artificial intelligence companies. According to data made available by OpenAI itself, the model was presented with around four thousand open problems, with ChatGPT Pro taking an average of three hours of computation per result, as part of a campaign launched – as the repository explains – when the mathematical tests routinely used by the company had ceased to provide a useful metric because the model was solving them all. Among the claims contained in the manuscripts are a proof of the Unique Games Conjecture – which has occupied a central place in theoretical computer science for over twenty years – and a zero-free region valid for every Dirichlet function L, whilst none of the papers address the five Millennium Problems that remain unsolved; according to a spokesperson, almost all the results are said to have stemmed from a single prompt given to a single agent, and many of them are reportedly not yet understood even by the company’s own mathematicians.

As the model is not publicly accessible, no one outside OpenAI is able to verify these claims, which is why, on 29 September, the advisory group on mathematics and artificial intelligence hosted by the Institute for Advanced Study in Princeton had asked the laboratories to accompany each result with the prompts from which it originated and the associated computational cost; OpenAI responded to this request by providing only an average of the computational effort required and by releasing ten abbreviated summaries of the model’s reasoning, without publishing any prompts. The error, announced on 7 October in the repository’s change log, consists of an incorrect sign within a manuscript on the algebraicity of Weil classes for certain abelian varieties of dimension eight, which invalidates a cancellation argument and, in turn, undermines the construction upon which two other papers were based, including the one that established the rational Hodge conjecture for products of K3 surfaces. The three manuscripts belonged to the family of results linked to the Hodge conjecture—the most closely watched in the entire catalogue—and the flawed one, dated 18 September, was among the oldest in the collection.

On the same day, OpenAI corrected a further fourteen manuscripts, rectifying proofs and clarifying statements and hypotheses, and updated the bibliographical references of a further thirteen, meaning the catalogue has been reduced from 722 to 719 titles, whilst the withdrawn versions remain available for consultation alongside a note describing the omission. A spokesperson attributed the discovery to an internal audit, without specifying who had identified the error, and assured that the review process, as is the case for any research manuscript, will continue until those papers for which no correction can be found are withdrawn. OpenAI usually responds to those who raise concerns by referring to Lean, an open-source language in which a proof is rewritten in rigorous form so that a programme can check every step; at the time of publication, however, only 162 of the 722 manuscripts had their main result formalised, and with the additions of 7 October, this figure rose to 300 main results out of 719 – just over 42 per cent – a proportion that has remained unchanged since then, given that the change log still contains only that single entry and the README repeats the same percentage. The company acknowledges that some of the non-formalised results may contain errors and explains that it published them without waiting for full formalisation on the recommendation of the advisory group itself, although a comparison with the repository index shows that almost everything that has been withdrawn or substantially revised was outside the part verified by Lean.

The fact that even the verified part requires caution is demonstrated by the precedent of 8 September, when OpenAI announced a 166-page proof on the formation of singularities in finite time in fluid equations, produced by around ten thousand agents in 88 hours and formalised in Lean in a further 17 hours; however, this concerns equations subjected to an external force, whereas the Millennium Problem requires the case without an external force to be addressed, which is why the Clay Institute does not consider it solved. On 6 October, the same day the 722 manuscripts appeared, Alexander Bastounis, Fabian Circelli and Anders C. Hansen published a preprint on arxiv entitled ‘Navier-Stokes lost in translation’, in which they argue that the proof formalised in Lean does not correspond to the proof written in natural language, which allegedly asserts more than the code verifies, and they cite other examples of erroneous translations produced by artificial intelligence systems alongside this case, going so far as to argue, on a theoretical level, that ensuring the fidelity of a formalisation is an intrinsically more difficult problem than the Turing halting problem.

As this is a preprint, which OpenAI does not appear to have replicated and whose abstract does not specify any particular files or versions, its conclusions must be scrutinised, bearing in mind that a formal proof following a different path from the one written leaves the result intact as long as the formalised statement coincides with the theorem one sought to prove, and that the problem only arises when the statement itself diverges. The issue, however, concerns all 719 manuscripts, since Lean guarantees that the code demonstrates what is written in the code, whilst establishing that what is written there coincides with the theorem of interest to mathematicians remains a human task that allows for no shortcuts; thus, that 42 per cent figure merely measures the proportion of the catalogue that has been scrutinised by the machine, without indicating how much of it is actually correct.

The retraction comes at the end of a month of tensions, which began with the dispute over priority that had accompanied the announcement regarding the Navier-Stokes equations, when it emerged that two mathematicians, Alpöge and Buckmaster, were working on the same problem, and continued on 11 September with the statement in which twenty-five Fields Medal winners, including Terence Tao, criticised the use of mathematical problems as a testing ground for the artificial intelligence industry. Ursula Martin, a mathematician at Oxford, compared the bulk publication of the 722 manuscripts to the submission of a messy first draft that the community would then have to sort out, and this comparison is borne out by the figures, given that at OpenAI each manuscript cost an average of three hours of computation, whilst verifying it requires weeks or months of specialist work that falls on researchers who did not ask for it. The company promises to fund workshops and conferences to help mathematicians understand the results and assures that it is working on releasing the model, whilst the advisory group has described the publication as the beginning of human understanding rather than its conclusion, suggesting that the bulk of the work has yet to begin and that it will fall to others to carry it out.

A sign error is perhaps the most human of all errors, one that befalls students sitting their first exam just as much as Fields Medal winners, and what this incident calls into question is rather the distribution of effort, because mathematics rests on a pact whereby whoever signs off on a proof understands and defends it, whilst the community undertakes to verify it; that pact falters when the author is a model that no one can question and the reviewers are mathematicians who had not asked for any of this. Lean was supposed to offer a way out by entrusting the verification to software, but the Navier–Stokes affair serves as a reminder that software only verifies what is submitted to it, and as long as OpenAI continues to produce theorems faster than the world can read them, the word ‘proven’ will have to be taken with a pinch of salt, even when certified by a computer.