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.
John Baez (Jun 02 2026 at 18:21):I hope y'all consider signing the Leiden Declaration, which is a statement of principles on the use of AI in math:
You can include comments along with your signature, and I had one minor nitpick about this passage:
- Technologies which affect the way in which mathematics is practiced may disturb the current system of incentives. The use of artificial intelligence — and thus also the sort of problems which it can address — may become incentivized for its own sake, disrupting our mechanisms for hiring, funding, and recognition.
Though I'm sure it wasn't meant to, this comes across as a bit complacent. Our current system of incentives is seriously flawed, so we should be working to improve it, not merely defending the status quo. We don't want AI companies to be twisting the incentives in mathematics - but university administrators, big journal oligopolies, and the military have been doing this for a long time, and that's no good either.
Kevin Carlson (Jun 02 2026 at 18:36):Not to mention the professionalization of the mathematics community itself, which goes back beyond those postwar interferences to around the turn of the century and incentivizes working on things because other people will agree it deserves a job relative to because you independently think it needs doing.
John Baez (Jun 02 2026 at 19:00):I urge all mathematicians to retire as soon as it's financially convenient. It's great being free.
Kevin Carlson (Jun 02 2026 at 21:30):Yes, one imagines so.
David Michael Roberts (Jun 03 2026 at 00:28):We can all eat cake when we do :-)
John Baez (Jun 03 2026 at 08:38):My remark may have come across as callous, because most of you youngsters can't afford to retire soon or even think about it. But for many oldsters who have worked all their life, retirement can feel like death: loss of institutional power and an externally imposed sense of purpose. So, one has to plan for it psychologically, not just financially. I wanted to let y'all know that it's not so bad. I enjoyed it a lot before I had to get a job again, to escape the US.
John Baez (Jun 03 2026 at 08:53):Bringing this back to AI:
I'm imagining there may be increased pressure for mathematicians to formalize their results using software - or at least any major results - because there's pressure for all LLM-proved results to be formalized, to minimize slop, and you can't really be sure which work has been done using LLMs.
What I now wonder is this: if a lot of older mathematicians face pressure to formalize their results in order to publish them, and they don't like competing with LLM-powered mathematicians, maybe they're be more inclined to retire!
John Baez (Jun 03 2026 at 08:56):Lest this seem a bit too futuristic (like a couple years too futuristic :wink:), check out my exchanges with an anonymous postdoc here. Here's a quote from them:
A few days ago, something extremely bizarre happened with me. A colleague X and myself were working on a problem and a third unrelated mathematician Y solved the entire project with ChatGPT 5.5 Pro. Y contacted X (whose work we were trying to generalize) and Y was generally nice about this. We're now publishing it together along with Y.
But the thing is, the finished paper is barely a paper in the traditional sense since almost the entire paper has been written by ChatGPT and Codex. I don't think it makes any sense to send it to a journal because no hard work has been put into it. X and myself were quite close to solving it and had it been written by humans this would have been a somewhat significant result that could have helped my career. Now it's just another addition to demonstrate AI's math capabilities.
I'm sure there are other such theorems getting actively purged by LLMs which could have been someone's life and career. I don't know where this is going and any advice on this strange world could be helpful. It feels frustrating and somewhat surreal honestly.
David Michael Roberts (Jun 03 2026 at 09:11):I'm sure there are other such theorems getting actively purged by LLMs which could have been someone's life and career
Hence Massot's oft-quoted comment
think the situation is pretty clear: AI companies, and especially MathInc, will indeed thoroughly bomb this area to turn it in a giant radioactive wasteland that will never be able to sustain life again, so we will never get the benefits expected from formalization (improved understanding and accessibility). I strongly advise young people to contribute to less shiny projects that are less likely to be destroyed.
John Baez (Jun 03 2026 at 09:27):For those not up on this stuff: that was slightly different.
Massot was complaining about how mathematicians working on carefully formalizing big known results could be beaten to the punch by AI companies who produce quick but messy and useless formalizations, as Math Inc did with the Kepler conjecture.
My anonymous correspondent was writing up a proof of a new theorem and got beaten to the punch by someone who proved it using an LLM. Luckily the person using an LLM was willing to join forces with my correspondent. But they still felt the result was devalued by this - no longer publishable.
(I argued that it should still be publishable if done right, and they decided to at least put it on the arXiv.)
John Baez (Jun 03 2026 at 09:28):But yeah, all these phenomena show how mathematicians feel under pressure.
David Michael Roberts (Jun 03 2026 at 09:54):Well, not different: the problem was that the AI company autoformalised stuff that students were working on formalising, but also had spent time painstakingly setting up the human-written framework that allowed the company to do the autoformalisation. So it's not scooping the first proof, but it still coming in and "taking the result", even if it's a formalisation project.
David Michael Roberts (Jun 03 2026 at 09:56):But yes, the output of the company was a bloated mess and it definitely "science by press release" rather than getting the intended result by AI in the end, in a less than satisfactory way.
John Baez (Jun 05 2026 at 13:46):The work I mentioned above has now appeared on the arXiv. I am happy that the authors followed the suggestions in the Leiden Declaration:
It looks like a very interesting result on the long-popular subject of dense sphere packings, and the paper looks well-written, at least at a first glance. But here's the part that's relevant here:
Statement on AI use.
The first two authors developed an approach combining Venkatesh’s [38] cyclotomic symmetries with Klartag’s [25] stochastic ellipsoid method. They focused on the case of modules of rank two over the ring of cyclotomic integers like in Venkatesh’s setup. This seemed to obtain a suboptimal lower bound on sphere packings which is in between Venkatesh’s lower bound and Klartag’s lower bound. Before moving to high ranks, the authors struggled to conclude if this is a miscalculation or a methodological problem in the setup.
Independently, the third author, inspired by the recent OpenAI announcement of an AI-generated disproof of the Erdős unit distance conjecture [1, 30], prompted the GPT-5.5 Pro model to extend Venkatesh’s construction to obtain improved lower bounds for high-dimensional sphere packings. The model proposed combining Venkatesh’s cyclotomic symmetries with Klartag’s stochastic ellipsoid method and, after further prompting to continue pushing on the approach, produced an improvement over the previous best bound. The model discovered the idea of letting the rank grow and successfully proved the bound given below.
The third author then contacted the first author, and the three authors joined forces to verify the proof and edit the writing, with ChatGPT and Codex used extensively in the process. The ancillary files accompanying this paper include a complete log of the ChatGPT conversation that led to the proof.
The first author is choosing to use a pseudonym.
Ryan Wisnesky (Jun 05 2026 at 14:19):In CS, there's some precedent for widespread AI use because there was a time that instead of AI, people would ask the internet for help (eg stack overflow) and those answers might be accidentally or deliberately wrong. So there, dealing with AI is a difference in quantity, not kind - 'trust AI the way you were already trusting stack overflow; trust the arXiv like you would a random person's website'. But I'm getting the sense from these many zulip chats on ai that there was never an equivalent time in math, when a culture of safety developed around the remixing of existing results by amateurs (programmers doing nothing but cut and paste good results being a true cliche now). I don't have an action to suggest by this, just wanted to point out a cultural difference between CS and math that I find fascinating.
John Baez (Jun 05 2026 at 14:57):Mathematicians like to pride themselves on what you might call the "chain of custody" of results being proved using results that have been proved... preferably with references. Fastidious mathematicians also want to understand all the proofs leading up to what they prove.
Once upon a time, computer-generated proofs - famously of the four-color theorem - challenged this attitude. I think we're more or less used to those now, and the fans of "formalization" may be unwilling to trust any result that hasn't been verified by a proof assistant. But AI poses different challenges.
(Purely mathematical challenges, not even counting all the issues like environmental damage, the use of AI by oligarchs to suck money out of the world economy, etc.)