You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Nathanael Arkor (Oct 07 2026 at 05:37):OpenAI shared a repository of mathematical results obtained by an internal AI model today. Here is a list of the results. Perhaps surprisingly, there are several results in category theory included.
The ones I spotted from skimming through:
Nathanael Arkor (Oct 07 2026 at 05:52):(I'm drawing attention to these only because I think it's wise to keep abreast of the progress of computer-assisted mathematics in one's own field, not because I endorse this practice.)
David Michael Roberts (Oct 07 2026 at 06:16):The first one of these was actually done mere days ago: https://arxiv.org/abs/2610.04096, posted by Kevin Coulembier and Johannes Flake
David Michael Roberts (Oct 07 2026 at 06:17):The main ideas in the proofs in Section 3 and Section 4 were originally obtained using
GPT-6 Astra, using as an input the formula in Equation (1.1), which was obtained previously using
extensive numerical experiments with the help of Claude 4.6–5 Opus.
David Michael Roberts (Oct 07 2026 at 06:22):And the OpenAI document doesn't cite them.
Nathanael Arkor (Oct 07 2026 at 06:58):And the OpenAI document doesn't cite them.
I would guess OpenAI obtained the result some time ago, generated a PDF, and then didn't update the PDF in the meantime to take into account any new results.
Nathanael Arkor (Oct 07 2026 at 06:59):But it sounds like the result was proven by ChatGPT either way; the only real difference was who wrote up the proof.
Matteo Capucci (he/him) (Oct 07 2026 at 08:15):God I didn't expect to be so disgusted by reading the repo. It's like seeing a forest being razed.
Matteo Capucci (he/him) (Oct 07 2026 at 08:16):They just dumped 300+ problems?
Morgan Rogers (he/him) (Oct 07 2026 at 08:18):Looks like they really took the advice from our colleagues seriously... :grimacing:
Nathanael Arkor (Oct 07 2026 at 08:20):They announced some time ago they had obtained this number of results and apparently consulted with some members of the mathematical community about the best way to proceed, so presumably there was a sufficiently significant number of people calling for this approach.
Cole Comfort (Oct 07 2026 at 08:40):Nathanael Arkor said:
OpenAI shared a repository of mathematical results obtained by an internal AI model today. Here is a list of the results. Perhaps surprisingly, there are several results in category theory included.
The ones I spotted from skimming through:
I sent this message to the authors of the new york times article on this subject:
Hello Kenneth and Siobhan,
Regarding your NYT article which was published today:
https://www.nytimes.com/2026/10/06/science/openai-math-problems.html
I am a category theorist and I would like to draw your attention to one of the problems that was claimed to be solved:
https://github.com/openai/math/blob/main/preprints/Fiber-functors-for-finite-symmetric-tensor-categories-in-positive-characteristic-September-24-2026/paper.pdf
The same result appears to recently have published on the arxiv preprint server, and openai do not cite the original authors:
https://arxiv.org/abs/2610.04096
This was brought to my attention by my colleague Dr. David Michael Roberts on the category theory zulip server:
https://categorytheory.zulipchat.com/#narrow/channel/241990-community.3A-discussion/topic/OpenAI.20preprint.20release/with/629770853
Here is an invite link to the forum which he raised this concern:
https://categorytheory.zulipchat.com/join/XXXXXXX
I would encourage you to contact the original authors, as they could have discussed their ideas with an openai model.
This is particularly concerning to myself and other mathematicians. This gives credence to Prof. Tristan Buckmaster who claimed that openai plagiarised his work in the openai announcement regarding the Navier-Stokes conjecture:
https://cims.nyu.edu/%7Etristanb/statement.pdf
Kind regards,
Dr. Cole Comfort
Cole Comfort (Oct 07 2026 at 08:52):@David Michael Roberts
In retrospect, I should have asked if you would want me to send this message to journalists.
But I think it is important that the press consult experts when discussing this subject.
David Michael Roberts (Oct 07 2026 at 08:56):@Cole Comfort not a problem. If the NYT wants to interview or mention me or whatever I don't mind. But really they should talk to Kevin C
Matteo Capucci (he/him) (Oct 07 2026 at 08:56):Nathanael Arkor said:
They announced some time ago they had obtained this number of results and apparently consulted with some members of the mathematical community about the best way to proceed, so presumably there was a sufficiently significant number of people calling for this approach.
Well they followed the advice, in theory: a public repo, a (ridicolously low) number of reasoning traces, and (ridicolously scarce) information on how the models were prompted. Honestly quite dumb of them to be so careless. It's going to backfire spectacularly IMO. But there's going to be casualties...
David Michael Roberts (Oct 07 2026 at 08:58):Someone I know who is an expert on one of the problems solved told me this:
this is so badly written, it's practically impossible to understand the ideas by looking at the paper.
David Michael Roberts (Oct 07 2026 at 08:58):A different problem to the Tannakian categories one, I will add
Cole Comfort (Oct 07 2026 at 09:00):It is possible that a large number of these claimed proofs are the result of mathematicians discussing similar or identical problems with openai's models.
Nathanael Arkor (Oct 07 2026 at 09:06):Even supposing that were the case, one might wonder to what extent the mathematicians have only themselves to blame. The AI companies don't try very hard to hide their attitude towards copyright, attribution, etc.
Cole Comfort (Oct 07 2026 at 09:10):I do not cast blame on mathematicians for discussions which they may have had with ai models. It is the standard practice in mathematics that the result of private discussions can not be published independently without appropriate acknowledgement. I don't see the ethical difference between an individual or company breaking this rule.
Nathanael Arkor (Oct 07 2026 at 09:11):There isn't an ethical difference. But OpenAI have proven themselves time and time again to be an unethical company.
Cole Comfort (Oct 07 2026 at 09:13):Maybe it is a good idea for users of openai products to disable the following setting:
Improve the model for everyone
Matteo Capucci (he/him) (Oct 07 2026 at 09:13):This is a pump&dump scheme deployed on a scientific field rather than a market.
Matteo Capucci (he/him) (Oct 07 2026 at 09:14):Cole Comfort said:
Maybe it is a good idea for users of openai products to disable the following setting:
Improve the model for everyone
Extraordinarily tendentious phrasing btw. 'Oh so you are selfish and want to keep your chats for yourself?'
David Michael Roberts (Oct 07 2026 at 09:14):It is deliberate psychological manipulation, yes
Morgan Rogers (he/him) (Oct 07 2026 at 09:17):Cole Comfort said:
Maybe it is a good idea for users of openai products to disable the following setting:
Improve the model for everyone
Another option I've personally found very effective is to not use OpenAI products
Cole Comfort (Oct 07 2026 at 09:18):It is possible that they would not respect if you declined. I may avoid using openai products in the future because their competitors appear to be less unethical.
Colin Zwanziger (Oct 07 2026 at 11:01):Cole Comfort said:
It is possible that they would not respect if you declined. I may avoid using openai products in the future because their competitors appear to be less unethical.
My understanding is that turning off the "improve the model" setting only gives partial protection, but there is typically a several month lag before any possible use of your data in a consumer model release. The internal model that generated these results used data up to July 3. With that said, I think these models are amazing tools and I'm using them a lot currently.
Colin Zwanziger (Oct 07 2026 at 11:07):David Michael Roberts said:
this is so badly written, it's practically impossible to understand the ideas by looking at the paper.
in such case it's probably better to use AI to unpack the result or demand tailored improvements in exposition...
in the worst case slop papers can be treated as glorified chain of thought for inter-AI communication
David Michael Roberts (Oct 07 2026 at 11:14):https://mastodon.social/@tobi_ohrmann/117399306174027471
out of interest, I looked at the preprint on the Benson-Etingof-Ostrik conjecture (which actually has been proved several days ago by humans). It's the exact same proof except at one substep. Interestingly, the human authors say that there is an alternative proof of this step in preperation by another human that was done with help of AI and which has all the bells and whistles from the Open AI version.. looks already quite similar to the NS situation and it's just one random pick
David Michael Roberts (Oct 07 2026 at 11:15):https://mathstodon.xyz/@jaycech3n/117399103849488234
The core of this is a purported proof of a conjecture by Simon Henry, that many have tried to prove before, and which implies the homotopy hypothesis. I've heard secondhand (by Thibaut Benjamin via Nick Hu) that the generated paper doesn't quite hold up, and also plagiarizes a recent small result. On the other hand Eric's (@ericfinster) assessment is more ambivalent, unsure if he'd like to weigh in here himself.
Nathanael Arkor (Oct 07 2026 at 12:54):It's the exact same proof except at one substep
looks already quite similar to the NS situation and it's just one random pick
Personally, I don't think the situation is comparable to the Navier--Stokes situation. Both proofs in this case were entirely generated by ChatGPT models, so it seems unsurprising the proof strategy would be almost identical.
Matteo Capucci (he/him) (Oct 07 2026 at 13:04):Nathanael Arkor said:
It's the exact same proof except at one substep
looks already quite similar to the NS situation and it's just one random pick
Personally, I don't think the situation is comparable to the Navier--Stokes situation. Both proofs in this case were entirely generated by ChatGPT models, so it seems unsurprising the proof strategy would be almost identical.
So did the N-S proofs by Buckmaster and Alpoge vs OpenAI. Except in both cases it looks like we have OpenAI's zero-humans in the loop prompting vs researcher who merely used ChatGPT to assist in key steps.
Nathanael Arkor (Oct 07 2026 at 13:23):No, even if the work developed by Buckmaster and Alpöge involved no human reasoning, their work made use of both ChatGPT and Claude, so it's much less reasonable to imagine that ChatGPT would come up with exactly the same proof strategy independently.
Matteo Capucci (he/him) (Oct 07 2026 at 16:48):Well but the prompts are different so it's not a given that ChatGPT would 'solve it the same way'. It seems Columbier and Flake had a very specific conjecture they used Astra for, whereas according to OAI little info about the math dump, they just one-shotted the statements
Matteo Capucci (he/him) (Oct 07 2026 at 16:49):Here 'prompts' is both the initial message and the other involvement of humans in the loop, which can perturb the trajectory of the model significantly
Nathanael Arkor (Oct 07 2026 at 17:06):I agree it's not a given, but I also think it's entirely conceivable.
V Slicer (Oct 07 2026 at 18:28):Matteo Capucci (he/him) said:
They just dumped 300+ problems?
And they say they're going to fund some conferences but to what end? Who's going to present the results? A virtual avatar? And who would discuss their related work at such a conference just to have OpenAI feed it right into their pipeline and "solve" it the next day? If anything going to such a conference might be signalling to OpenAI to look into your work because it's a good indication it's related, and they're obviously looking for more problems to ‘make number go up.’
V Slicer (Oct 07 2026 at 18:32):Matteo Capucci (he/him) said:
God I didn't expect to be so disgusted by reading the repo. It's like seeing a forest being razed.
Same here, I had a stomach-turning, visceral reaction reading the overview…
V Slicer (Oct 07 2026 at 18:42):Nathanael Arkor said:
No, even if the work developed by Buckmaster and Alpöge involved no human reasoning, their work made use of both ChatGPT and Claude, so it's much less reasonable to imagine that ChatGPT would come up with exactly the same proof strategy independently.
In the interview Buckmaster reveals that OpenAI not only lied to them on a video call, but that OpenAI ‘only’ used a swarm of 100 bots to reach their forcing result and then I believe a bot swarm of 10000 for the more general N-S result. They find this very suspicious and it leads them to believe that OpenAI used their work. So there might have been humans in the loop, but in the worst way possible: guiding the swarm to take the same path as Buckmaster and Alpöge to scoop their result.
https://www.youtube.com/watch?v=Mzbtj5nkMXI
V Slicer (Oct 07 2026 at 18:49):John Baez said:
OpenAI dropped 722 new math papers; number 312 proves a version of Grothendieck's homotopy hypothesis.
More discussion here.
Reading through that list is honestly jarring.
Colin Zwanziger (Oct 07 2026 at 19:03):David Michael Roberts said:
https://mathstodon.xyz/@jaycech3n/117399103849488234
The core of this is a purported proof of a conjecture by Simon Henry, that many have tried to prove before, and which implies the homotopy hypothesis. I've heard secondhand (by Thibaut Benjamin via Nick Hu) that the generated paper doesn't quite hold up, and also plagiarizes a recent small result. On the other hand Eric's (@ericfinster) assessment is more ambivalent, unsure if he'd like to weigh in here himself.
Thibaut Benjamin chimed in to clarify
I was made aware I was cited on this, so let me clarify my position, which I think has been slightly exaggerated here :)
- All this is all based on early impressions, at the time I am still processing what's in the paper (and even more so this morning)
- As far as I can tell, the proof strategy is roughly the same everyone I know who's thought of the problem has been trying (myself included)
- I think Prop 4.3 is where the real meat is. It's a problem that I know to be hard and technical (combinatorial) and I cannot yet understand the provided proof. What I can say is that said proof seems far below the combinatorial complexity I would expect, which I find suspect.
- I was made aware since this morning that there is a Lean artefact accompanying this paper. Early work by my colleagues seems to indicate that the lean result indeed corresponds to the claimed result in the paper.
https://mathstodon.xyz/@thiben/117400709229046075
John Baez (Oct 08 2026 at 08:19):Many of these results were not yet verified using Lean, so some are being withdrawn:
In “Algebraicity of Weil classes on split abelian eightfolds” a sign error invalidates a stabilization-trace cancellation argument and the construction used by two dependent papers. As a result, we have withdrawn the following three manuscripts:
- Algebraicity of Weil classes on split abelian eightfolds
- Algebraicity of Kuga–Satake Correspondences for K3 Surfaces
- The rational Hodge conjecture for products of K3 surfaces
The withdrawn papers now carry notices explaining the gap and linking to the archived manuscripts.
Others are being corrected.
Morgan Rogers (he/him) (Oct 08 2026 at 08:28):Imagining the people doing the correcting brings to mind the people that work to collect plastic bottles on huge heaps of imported trash, trying to recover value from mass-produced garbage.
John Baez (Oct 08 2026 at 08:31):Here's an intriguing paper on the arXiv:
I haven't verified this paper, but here's part of what it says:
It is natural to ask whether this formalisation in Lean represents a semantically faithful translation of the NL [natural language] paper, so that we can conclude that the NL paper represents a correct proof? Interestingly, OpenAI’s announced proof becomes a great source for examples of mistranslations, exactly as pointed out in §2. In particular, the Lean formalisation does not represent a semantically faithful translation of the NL paper, meaning that the Lean formalisation provides no guarantee that the NL proof is correct. We provide several examples below.
John Baez (Oct 08 2026 at 08:33):I think the claim is not that the Lean-verified proof is not really a proof of Navier-Stokes, just that the proof you can read in English has mistakes.
Matteo Capucci (he/him) (Oct 08 2026 at 08:48):Morgan Rogers (he/him) said:
Imagining the people doing the correcting brings to mind the people that work to collect plastic bottles on huge heaps of imported trash, trying to recover value from mass-produced garbage.
What isn't clear from the (consistently awful) communications is whether these mistakes were found by humans or by them?
Morgan Rogers (he/him) (Oct 08 2026 at 09:01):Right, I suppose it is optimistic to suppose that it's mainly humans.
Notification Bot (Oct 08 2026 at 09:01):8 messages were moved here from #community: general > AI-generated papers by Morgan Rogers (he/him).
Damiano Mazza (Oct 08 2026 at 09:14):Isn't this thread on the same exact topic as "OpenAI preprint release"? Shouldn't they be merged?
Nathanael Arkor (Oct 08 2026 at 09:20):I merged the topics, although I didn't spot that the earliest timestamps were interleaved, so apologies for any confusion that might cause.
Nathanael Arkor (Oct 08 2026 at 09:21):John Baez said:
I think the claim is not that the Lean-verified proof is not really a proof of Navier-Stokes, just that the proof you can read in English has mistakes.
That's not quite the claim either: the claim is that the natural language proof is different from the Lean-verified proof. It may be that both proofs are valid, but at least somewhat different. (Of course, it could also be that the natural language proof does have mistakes, since it hasn't been formally verified or extensively checked by humans yet.)
Nathanael Arkor (Oct 08 2026 at 09:22):Matteo Capucci (he/him) said:
What isn't clear from the (consistently awful) communications is whether these mistakes were found by humans or by them?
From discussion on Twitter, it sounded to me like the mistakes were found by people outside OpenAI, but using AI.
Damiano Mazza (Oct 08 2026 at 09:25):Nathanael Arkor said:
I merged the topics, although I didn't spot that the earliest timestamps were interleaved, so apologies for any confusion that might cause.
Thanks Nathanael! I think everything is consistent, the only weird thing in the thread now is @John Baez's message from yesterday at 18:10 (my local time) saying "OpenAI dropped 722 new math papers", which is just a repetition of your original post so it would look puzzling from someone reading the thread from the top. But I don't think the merge causes any confusion otherwise.
Matteo Capucci (he/him) (Oct 08 2026 at 09:36):Nathanael Arkor said:
From discussion on Twitter, it sounded to me like the mistakes were found by people outside OpenAI, but using AI.
So lol they didn't even check the outputs of the models with other models? Yikes!
David Michael Roberts (Oct 08 2026 at 09:50):https://karagila.org/2026/openai-pp/
Nicolai Kraus (Oct 08 2026 at 10:24):(edit: Removed this comment because it was a duplicate of a comment above. Sorry.)
Nathanael Arkor (Oct 08 2026 at 10:25):(This is what I wrote above.)
John Baez (Oct 08 2026 at 12:41):Nathanael Arkor said:
John Baez said:
I think the claim is not that the Lean-verified proof is not really a proof of Navier-Stokes, just that the proof you can read in English has mistakes.
That's not quite the claim either: the claim is that the natural language proof is different from the Lean-verified proof. It may be that both proofs are valid, but at least somewhat different. (Of course, it could also be that the natural language proof does have mistakes, since it hasn't been formally verified or extensively checked by humans yet.)
You're right. The paper gives an example of a true statement with an incorrect natural-language proof that gets autoformalized to a correct Lean proof (Example 2.2). But this example is not from the proof of Navier-Stokes, and they don't claim this phenomenon has been seen in the Navier-Stokes proof.
V Slicer (Oct 08 2026 at 12:56):Nathanael Arkor said:
John Baez said:
I think the claim is not that the Lean-verified proof is not really a proof of Navier-Stokes, just that the proof you can read in English has mistakes.
That's not quite the claim either: the claim is that the natural language proof is different from the Lean-verified proof. It may be that both proofs are valid, but at least somewhat different. (Of course, it could also be that the natural language proof does have mistakes, since it hasn't been formally verified or extensively checked by humans yet.)
This is exactly the issue we were discussing a few months ago, we can be reasonably sure something is being proven with the Lean proof but mathematicians still need to go over it and confirm it proves what is claimed to have been proven.
Ivan Di Liberti (Oct 08 2026 at 13:03):Cole Comfort said:
t
To clarify, this is only part of the needed procedure to follow in order for your model to not be trained on your chats.
Matteo Capucci (he/him) (Oct 08 2026 at 14:10):What's the rest?
Morgan Rogers (he/him) (Oct 08 2026 at 15:54):@Ivan Di Liberti you didn't clarify much :stuck_out_tongue_wink:
David Egolf (he/him) (Oct 08 2026 at 23:09):Here's a link to a collection of reactions to the situation: https://proofsandprompts.com/2026/10/08/100-reactions-to-100-solutions/
David Egolf (he/him) (Oct 08 2026 at 23:12):I especially appreciated part of what Peter Scholze said:
We should remember that we are all in this together; mathematics is a marathon, not a sprint; and the goal is and always will be the human understanding of mathematics, which will invariably take time.
Patrick Nicodemus (Oct 09 2026 at 01:54):John Baez said:
I think the claim is not that the Lean-verified proof is not really a proof of Navier-Stokes, just that the proof you can read in English has mistakes.
Although Navier-Stokes is proven in Lean, it does sound like the paper contains a number of theorems that are not proven in Lean, because the Lean version is weaker.
David Michael Roberts (Oct 09 2026 at 03:17):After the paper was written, the author learned that the same result was also proved
independently and by a different method by Ningyi Li [7 ]. The result is also contained in a
paper [8 ] released by OpenAI on October 6, 2026, in which the proof strategy and specific choices
of notation are identical to a preliminary version of the present paper that was uploaded to
ChatGPT on September 8, 2026.
https://arxiv.org/abs/2610.10072
David Michael Roberts (Oct 09 2026 at 03:18):This was posted on 7 October. Also in there:
Statement on AI Use
The original idea of applying Chai’s rigidity results to the Hovey–Strickland conjecture arose
from the author’s work on questions related to Shimura varieties. In that context, the author
had become familiar with Chai’s methods for studying invariant formal subvarieties and density
phenomena. This led the author to consider whether these methods could be applied to the
action of the Morava stabilizer group on Lubin–Tate deformation spaces, and thereby to the
Hovey–Strickland conjecture.
The main conceptual route originated from the author’s observation described above. After the
proof of the general statement was formulated, ChatGPT was used on September 8, 2026 to check
that the author’s method works in height-3 case. AI assistance was subsequently used for proof
auditing. On September 10, 2026, during a review of the argument, ChatGPT identified a problem
in the original proof of theorem 6.1 concerning the passage from infinite Cartier-coordinate data
to finite jets. It suggested the fixed-jet repair developed in Appendix A. The resulting argument
was then rewritten, checked, and incorporated into the proof by the author. This is the only part
of the proof whose initial argument was generated by AI.
David Michael Roberts (Oct 09 2026 at 03:19):So now at least two papers that I know of existed on the results from OpenAI before the release of the big list. How many others?
Ivan Di Liberti (Oct 09 2026 at 05:38):Matteo Capucci (he/him) said:
What's the rest?
https://privacy.openai.com/policies/en/ and follow the steps.
Matteo Capucci (he/him) (Oct 09 2026 at 08:58):David Michael Roberts said:
So now at least two papers that I know of existed on the results from OpenAI before the release of the big list. How many others?
We should make a public database of these...
Zoltan A. Kocsis (Z.A.K.) (Oct 09 2026 at 09:00):@Ivan Di Liberti One should give a disclaimer here: opting out is useful, but also the wording is seriously misleading and can create a false sense of security.
These opt-outs don't opt out from OpenAI using your content to improve and develop their services and conduct research. Conducting research is of course a maximally broad, and very relevant mandate. All uses that aren't literally training a model (evals, benchmarking, distillation, etc.) remain authorized with the toggle off. The mathematical substance of your sessions can still lawfully flow into OpenAI's internal work through research, evaluation, de-identified reuse, or human review all without violating the policy as written.
Zoltan A. Kocsis (Z.A.K.) (Oct 09 2026 at 09:03):It's easy to do things that can recreate the pattern observed in the OpenAI release even if they haven't literally trained on the data.
For example, if I build an evaluation set from your sessions and test internal models against it ("I wonder, can our new model improve upon incomplete proofs or partial results written by an older model?"), that's not training on your data. But the resulting proofs will very much be followup work from user content.
Ivan Di Liberti (Oct 09 2026 at 10:20):Thanks Zoltan.
David Michael Roberts (Oct 10 2026 at 05:56):Hugo Duminil-Copin said in a talk that because he had wind of the dump with some notice, this paper was rushed out: https://arxiv.org/abs/2610.08507 I think landing the same day or just before.
AI use statement. No mathematical content was generated or found with the assis-
tance of artificial intelligence.
and this was one of the problems in the dump.
The proof in the dump, he said, was essentially the same.
Matteo Capucci (he/him) (Oct 10 2026 at 08:27):David Michael Roberts said:
https://www.youtube.com/watch?v=GweKOBSJvEY mathematics being discussed on mainstream news is pretty astonishing
Thanks very interesting. This is exactly what we should be doing, talk to the public.
Matteo Capucci (he/him) (Oct 10 2026 at 08:29):He was pretty ill-prepared to the very, obvious first question which was: why does regularity of N-S matter at all? That would have been a good place where to implant the idea that it does not and that's the point: solving it is just a benchmark for the fluid dynamics community on how much they understand these equations, and it's this understanding that then can be applied and makes mathematics worthwile.
Matteo Capucci (he/him) (Oct 10 2026 at 08:31):It's worth noting that there is a subtantial crowd of people who would be happy to see funding for film studies and other things they believe are 'useless' go...
Zoltan A. Kocsis (Z.A.K.) (Oct 12 2026 at 03:13):It's worth noting that there is a subtantial crowd of people who would be happy to see funding for film studies and other things they believe are 'useless' go...
Agreed. What I alluded to in the other thread is that this crowd is clearly not substantial enough to make the appropriate level of state funding for film studies (or other fields whose outputs are not clearly measured in "results primarily useful to the associated industries"), as determined by the taxpayers, zero.
Based on the German Research Funding Atlas, the DFG allocated literary studies 136m EUR between 2020-2022 (Figure 5-6), and mathematics 305m EUR (Figure 5-10). If funding was to drop down to the level of literary studies (or even philosophy w/ its 77M) because said crowd calls for reduced funding, it would still not be an existential threat to the future of academic mathematics.
Zoltan A. Kocsis (Z.A.K.) (Oct 12 2026 at 03:19):It is plausible (though I think unlikely) that the opinion of said crowd eventually becomes mainstream enough that the funding of all academia drops to zero. But if that's the concern, I doubt "OpenAI's agents got good at proving theorems specifically" will be a big factor.
Matteo Capucci (he/him) (Oct 12 2026 at 09:20):Zoltan A. Kocsis (Z.A.K.) said:
this crowd is clearly not substantial enough to make the appropriate level of state funding for film studies (or other fields whose outputs are not clearly measured in "results primarily useful to the associated industries"), as determined by the taxpayers, zero.
Well maybe in Europe but in the US the crowd did seize power and wreak havoc in funding... But I welcome the optimism, I don't think the US path is inevitable (and even there, research took a hit but it did not collapse)
John Baez (Oct 12 2026 at 11:18):Federal funding of research has largely collapsed in the US, in part because the executive branch is slow-walking the funds:
This shows 2026 National Science Foundation funding that's been released so far, as a percentage of 2025 funding, and as a function of time. So, you'll see that in July, mathematical and physical sciences funding had reached 30% of what it was last year. For research on education it's about 6%, because the Trump administration especially hates that. I'm sorry I don't have more recent data.
John Baez (Oct 12 2026 at 11:18):Most of this slowdown is illegal, by the way.
John Baez (Oct 12 2026 at 11:24):Meanwhile here in the UK there's a kind of collapse of the university system going on.
Domestic undergraduate tuition fees, capped at £9,250 since 2017/18—a freeze inherited and extended by successive governments—have lost over 25% in real terms to inflation by 2026. This shortfall forced reliance on international fees, which subsidize 40-50% of income at many institutions and cover research and infrastructure.
Post-Brexit and amid global competition, 2023 visa restrictions—banning most dependants and tightening graduate routes—slashed international visas by 39% in 2023/24, with declines persisting into 2026.
So, one of my fears about OpenAI's big theorem dump is that it will give (highly paid and expanding) university administrations the excuse to lay off mathematics faculty.
Matteo Capucci (he/him) (Oct 12 2026 at 14:13):John Baez said:
Federal funding of research has largely collapsed in the US
ah damn, there you go... no optimism allowed these days
Morgan Rogers (he/him) (Oct 12 2026 at 15:02):Well here in France the students aren't taking things lying down at least :wink:
V Slicer (Oct 13 2026 at 17:27):Matteo Capucci (he/him) said:
John Baez said:
Federal funding of research has largely collapsed in the US
ah damn, there you go... no optimism allowed these days
If there's any cause for optimism it's what Morgan Rogers (he/him) said:
Well here in France the students aren't taking things lying down at least :wink:
And that it's spreading to other places, like to Belgium and Greece, where there are many proletarians, students, staff and those in solidarity with them, taking to the streets. There are multiple ongoing university occupations, in Argentina and Italy for example. At the end of September German students were demonstrating against militarism and forced conscription. And while not specifically student-led, Japan has been seeing demonstrations against militarism. There are continuing housing protests and encampments in Spain, as well as protests in Brazil. Some are already comparing it to the Hot Autumn in Italy and the May '68 uprising in France, and corresponding wave of events all over the world. We can see students, or I should perhaps say would be communards, channeling the Paris Commune of 1871, writing ‘Vive la Commune’ on the buildings they are occupying. Nothing is certain, but it does feel like many are fed up and can't see anymore how things can go on as it has, for many different reasons and are finding each other.
“The rebels of the Paris Commune, of the Shanghai Commune, of Berlin in 1918 and Bologna in 1977 and Argentina in 2001, act for themselves and others—not just Paris or Shanghai or Bologna or Buenos Aires or Cairo, but Paris and Shanghai and Bologna and Buenos Aires and Cairo. Inasmuch as they act in such a way as to make possible a later overcoming of class itself, then, they act on behalf of all proletarians, even and especially those not yet born into dispossession. In this manner, to the extent that they introduce something new into the class struggle, something imitable, they inspire sympathy, solidarity, and imitation far and wide.
As without, so within. The self of self-organization is spectral, dissolving at any moment into the frayed ends of individual selves. This is why all attempts to represent, to count, to fix the revolutionary camp in place, however defined, must fail. In collective action, people together believe what individually they doubt, making the boundaries of such actions indiscernible. Self-organization is a kind of fanatic reason—something is rational because in collective action people make it so.” (Jasper Bernes, The Future of Revolution, p28)
Joe Moeller (Oct 13 2026 at 19:37):This is a huge piece of why I said at the ACT community discussion session that criticism of US based people over taking military funding should be accompanied with a huge scoop of nuance. Yes, this has a selfish component since I'm funded through the airforce. But it is the closest thing to secure funding right now. And many people in that funding structure are sympathetic, to say the least.
Morgan Rogers (he/him) (Oct 13 2026 at 20:19):@Joe Moeller by "this" do you mean the collapsing federal funding?
Joe Moeller (Oct 13 2026 at 20:19):Yes
Colin Zwanziger (Oct 16 2026 at 15:28):Has anyone weighed in recently on the claimed homotopy hypothesis proof?
Jean-Baptiste Vienney (Oct 16 2026 at 16:08):I briefly talked with Simon Henry the other day as he is a professor at uOttawa and I'm a student there. He said he was still looking into it with other people but the proof looked correct, although the paper is not well-written.