What even is mathematical output?
It’s been nearly a week since the dump of the GitHub repository with over 700 documents and (far fewer) Lean formalisations of AI-generated proofs, but it’s felt a lot longer. My own views on use of AI are mixed. I use it for my day job, we formalise things (previously in Isabelle, now in Lean) that we are implementing, and which will never be made public. I have played around with AI to fill in my understanding of background material for a research paper I’m writing, and to try to hunt for references for things that are difficult to find, and to generate some code that calculates something in a specialist language I didn’t know. I have used it to translate and extract material out of old scanned documents. But I am loath to just get it to prove things I want to know. A couple of years back I did, when the systems were much more flaky, and eventually I ended up just deriving what I got out of it by hand from scratch, as I lost the transcript and I needed a proof anyway. I choose not to get it to draft or write my papers for me, as I find it just insufferable.
I have spent perhaps more time that I should have trying to get a measure of people’s takes; I didn’t want to comment at the time. Some are obviously really interested in mining the 700+ documents for insights, or for taking them and improving the result (for instance the multiplication algorithm complexity bound has been dropping rapidly, but these are perhaps mostly just announced in posts on X/Twitter). Some people want to run AI over the system and give appropriate credit rather than letting authors of cited work be buried under the size of the pile. Perhaps an even more worthy task would be figuring out who wasn’t cited for their ideas that were used. This is aside from people who had already worked on and solved the problems, sometimes with AI, and whose work wasn’t recognised. Others would like to ignore the material and not donate their expertise and time freely to help the company disseminate or (more likely) give feedback to the model that produced the material in the first place to improve it.
A lot of ink has been spent trying to think about what it is that the pure mathematics research community actually values, if being suddenly having hundreds of claimed results being dropped on us isn’t actually what we wanted. Many have said, rightly, that the mere fact of the theorem being true or false is not actually that useful. The value in that binary piece of information is that it gives confidence that there really is a fact of the matter that is (apparently) known, and can liberate people to really let rip. But the actual benefit comes from understanding the mathematics, because it adds to our toolkit, triggers associations to other parts of mathematics, opens new questions etc. But one might, as an outsider, feel that saying that no, the AI can say it’s true, but we want this fluffy concept of “understanding” instead, is a bit of a soft, reactionary excuse. It’s actually very difficult to pin down on paper what clarity and understanding is for research mathematics. To step back, it’s really nontrivial to assess students’ understanding of mathematical ideas they are learning and being assessed on, and those are ideas that people have known for centuries or even millennia, in some form, and which the assessors (teachers, lecturers, examiners) have expertise, fluency, mastery etc in. Now try to imagine how you assess someone’s understanding on mathematics when they have just synthesized a new theoretical framework that only they (or a small group of collaborators) understand. What is the actual method by which we can appreciate someone’s understanding of ideas you are hearing for the first time? I argue that it is in the communication of those ideas.
To draw a parallel, when Shinichi Mochizuki released his four papers on Inter-universal Teichmüller Theory in 2012, the excitement that he had built a framework to prove the abc conjecture was real, but the papers themselves as written did not help communicate the ideas. There were eventually workshops, and in-person communication (via video feed) did not improve matters. Leaving aside the actual correctness or otherwise, if experts in the topic are getting frustrated with the exposition for being unclear, and can’t tell if you have actually proved the claims or not, that’s a failure of process. My long-held view is that the papers could and should have been rewritten to be simpler (they absolutely could have been) and clearer, in the years that followed, as a form of service to the community that was trying to understand them. It was a common position that if experts can’t read the papers because they are not written clearly enough, the proof hasn’t been communicated, and as a result the theorem cannot have been held to be established.
I have said before that I like the fact even pure mathematics actually produces material output. For most research, this is not images, or physical objects: the thing that is created is the writing, the paper, or, sometimes, the board presentation or slides. One of the best talks I ever saw was a keynote at CT2014, which use the blackboards in the lecture hall to perfection, the layout and design of the talk as presented used exactly all the available space once, and material that needed to be referred to late in the talk was just there to be gestured at. Sadly, I can’t quite recall who it was! One stand-out creator of slides, if he’ll pardon me for singling him out, is Bryce Clarke (eg, these slides from his CT2025 talk).
But, on the whole, it is mathematical writing that stands the test of time. I can pick up (a translation of) Richard Dedekind’s 1872 paper introducing what are now called Dedekind cuts in order to define the real numbers, and it is a masterpiece (in my opinion) of insightful and clear writing. I can read Grothendieck’s 1957 Tôhoku paper (even though my French is very impoverished) and the brilliance of it shines through. I once wrote:
Mathematical exposition, if it is to be effective, must give both an intuitive picture of difficult ideas and a precise technical description of their meaning. The best writers do this seamlessly.
—A Crisis of Identification
Even though mathematical ideas get digested, get filtered though many minds, there is a reason reading old mathematical texts is still worthwhile. I recall Manjul Bhargava was inspired by reading Gauss’ 1801 monograph Disquisitiones Arithmeticae to come up with new insights that were left to be gleaned by generations of mathematicians who had only read downstream treatments. It is (largely) by our writings that the quality of a mathematician’s work is assessed, though it’s recognised that this is sometimes by the proxy of a journal, whose referees and editors have ideally given the paper its best chance. And it is the permanent record by which they can create a legacy.
So this brings us back to the dump. Like many others last week, I trawled through this list, even just out of curiosity. A standout to me was the uniform zero-free region in the critical strip of the Riemann zeta function, as I’m aware from the work of my Australian colleague Tim Trudgian and colleagues (eg this paper from March this year) on getting larger, but still decaying, such regions. The other one was the establishment of the Grothendieck’s homotopy hypothesis for the version of -groupoids extracted from the first part of Grothendieck’s Pursuing Stacks, the actual original letter to Daniel Quillen. This was interesting purely from the point of view of history: it establishes that Grothendieck’s definition of -groupoids, which is used by practically no one, was actually correct. The actual result proved was a technical lemma conjectured by Simon Henry, which by a longer chain of reasoning suffices to establish the homotopy hypothesis in this setting. I will say that I have not actually read any of the papers, largely because none of them are on things I actually work on, or are close enough that I need to read them.
Having established that mathematicians care about what each other actually write, then what do we say about the over 700 pdf documents that landed last week? Certainly people expect AI to write slop. But you get assessments like this from experts on the material they are looking at:
A senior colleague of mine found one of his favourite problems among those solved and attempted to read the accompanying paper. He told me it was so unintelligible that, had he received it as an editor at a mathematics journal, “it would have gone straight into the bin”.
—Melissa Lee, Monash University (writing at The Conversation)
and this:
I took a brief look at the preprint released by OpenAI […]. It sucked. It is unclear, muddled, and has a strange structure. The terminology is “a bit off”, there are theorems that I would not expect to be proved, that are also stated in a very strange manner. Lemma 7.4, again, is not something you’d expect to see in a paper like this, the same goes to Lemma 8.1.
[….]
No, if this was an academic paper submitted to a journal, it should be issued a desk rejection for the quality. The onus is always on the author to conform and adhere to the communications level. Much like a paper written in Swedish would likely be rejected outright from the Proceedings of the American Mathematical Society, because the onus is on the authors to make it accessible for the readers.
—Asaf Karagila (blog post)
and this
“To the extent I have looked, I would not bet any money that either has a correct proof. Both read like papers I would immediately reject were I a referee, as both seem mainly filled with awkward proofs of well known facts with nothing that motivates.”
—Nick Kuhn (ALG-TOP mailing list)
and this
But the more I thought about it, the more annoyed I became. What bothers me most is the double standard.
Whenever I referee a paper, or receive a thesis or project from a student, I apply the same standards that most of us do. If a paper or thesis is so badly written that I cannot get past the first page without considerable effort, I reject it and ask for a new, readable version.
With these AI-generated papers, I feel that we, as a community, are not applying the same standards of quality and rigour. They can simply release multiple 100+ page papers claiming to have solved this or that problem, often with redundant arguments, unclear logical structure, multiple dead ends, and strange or unsettling terminology — in other words, slop.
—Enrico Fatighenti (self-described as ‘not a Luddite’ who uses AI for various tasks) Proofs and Prompts
and this
It’s clear many papers were never reviewed by a human: for instance, I took their example #254 (an Artin group with no CAT(0) action): their group has 116 generators, but after feeding it to Astra, in 10 minutes I got a new example with 12 generators. Clearly, they were in a rush to post the big drop, prioritizing quantity over quality…Why?
—Giulio Tiozzo, Proofs and Prompts
There are of course reactions by people who are willing to look past the slop, for whom the results are too valuable to ignore. But the fact of the matter is that the output can’t have been refined past the original generation, which is what (ideally) mathematicians do for their own work once the results are generated. One particularly cynical view is that this is like outputting a giant calculation and then leaving the understanding to the people who are trying to get some value out of it. In fact, it is just a giant calculation, just on a scale remote from any kind of personal experience, and then distilled into some output in symbols that approximates ordinary writing.
I was much amused by the parody account @Endings500 that sprang up on X/Twitter last week, and this was a small amount of amusement when (unformalised) papers had to be withdrawn from the dump for having errors:
https://twitter.com/Endings500/status/2108214530614677952
To stretch the film analogy to breaking point, it’s not just that there is some content like a film showing only the last 10 minutes, it’s that the film is of a similar quality to Plan 9 from Outer Space (“justly celebrated for its staggering ineptitude”).
One might, however, take heart in the fact that a bunch (by all means not all) of the claims were formalised in Lean. As much as people are getting mileage out of the recent preprint showing that the Navier–Stokes formalisation doesn’t match the pdf describing the proof, that is really just a proof of concept: autoformalisation of a paper argument really needs double-checking against the written version to see if they match, and one or the other should be adjusted so they match. It says little about the results until an expert checks one or both.
However, one doesn’t need to be a Lean expert to see that code like this (the entirety of the file OrdinaryArchimedeanTwistBasic.lean):
import Mathlib
namespace OAI
noncomputable section
open scoped BigOperators
open MeasureTheory intervalIntegral
open Finset
open Finset Nat ArithmeticFunction
open scoped ArithmeticFunction.Moebius
open Filter
open MeasureTheory Filter
open MeasureTheory
open MeasureTheory Set
open Set MeasureTheory Complex
open Set
open Finset Filter
namespace OrdinaryArchimedeanTwist
end OrdinaryArchimedeanTwist
end
end OAI
literally does nothing. This is one of the Lean files in the repository for the dump (thanks to Joseph Meyers in the Lean Zulip chat server for pointing some of these ridiculous files out). A basic deterministic code cleanliness linter would have picked these up, let alone an audit by the all-power internal model of its own output. Another one, pointed out by Sébastien Gouëzel in the Lean Zulip goes like this:
import OAI.Dynamics.TriangleBilliards.SpatialRigidity
namespace OAI
open MeasureTheory Set
open scoped ENNReal symmDiff
noncomputable section
open MeasureTheory Set Filter Function Metric
open scoped Topology Convolution ContDiff
noncomputable section
open MeasureTheory Set
open scoped ENNReal
noncomputable section
open MeasureTheory Set Filter BoundedContinuousFunction
open scoped ENNReal Topology ComplexConjugate
noncomputable section
open MeasureTheory Set Filter
open scoped Topology ComplexConjugate
noncomputable section
open MeasureTheory Filter
open scoped ComplexConjugate
noncomputable section
open MeasureTheory Filter Set
open scoped Topology ComplexConjugate
noncomputable section
open Filter Finset Set
open scoped Topology BigOperators
noncomputable section
open MeasureTheory Filter Set
open scoped Topology ContDiff NNReal
open MeasureTheory Filter Set
open scoped Topology ComplexConjugate
noncomputable section
open Filter Set
open scoped Topology
noncomputable section
Again, the pointless repetition is far below the quality I would expect even in my own use of a less-powerful AI system to generate Lean code locally. The apparent complete lack of care to do undergraduate-level code clean-up is striking, even if the code compiles ok. One can then perhaps extrapolate to the quality of the English writing that the system has put out.
And if mathematicians are judged on their writing, as the medium to communicate ideas, to give others the hard-to-describe understanding, and mathematics is judged on how clearly it is written, I hope you, dear reader, can appreciate at least one aspect of why the dump of over 700 long documents of this nature is not just frustrating, but insulting.
#AI