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 (May 29 2026 at 18:25):Here's an interesting discussion of the possible dangers of AI companies that formalize famous results in Lean in ways that humans can't easily understand or benefit from, meanwhile denying mathematicians the academic credit for being the first to so:
It got spicy when Patrick Massot wrote:
I 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.
I think the solution is for famous and/or institutionally powerful mathematicians to keep emphasizing the importance of understanding in mathematics - and rewarding those who pursue it.
Ryan Wisnesky (May 29 2026 at 18:36):