A proof with no warranty
Some view the future of mathematics as a dystopian arcade of button-pressing, staring at a screen waiting for AI to do the thinking for us, with the main human involvement limited to asking the initial question and offering sporadic words of encouragement. Each new proof is then thrown into a repository, to only ever be read by other AIs, and the human presses the next button.
I believe Erdős would have found this future grim indeed, and the antithesis of mathematics as he practised it. Use AI as you like — but do not abandon mathematics as a human activity.
Don’t solve a problem for the sake of it; life is too short to spend it doing things that don’t matter to you.
Find a question that is meaningful to you, find other humans who are interested in it, and talk about it. Be confused, be stuck, be inspired. Find a messy proof, then find a better one. Get tired, get hungry, get into a flow state. Argue, laugh, give up, drink some coffee, and attack it again.
Be human. Let your brain be open.
Bloom, who runs the Erdős problems site, is freezing new problem comments and proof claims there, and no longer displaying whether a problem is open or solved. What the comments had become:
The main way that people publicly interact with the site now is to advertise their AI-generated proofs, often without any attempt to explain them, but as a way to record a (increasingly meaningless) priority claim.
If it turns out mathematicians can indeed keep mathematics a very human activity, this is one of the main differences between software and mathematics. Even before AI, some (but not all) open source creators and maintainers held the view that the point of open source is that we don’t need to collaborate. Rich Hickey, the creator of Clojure, put it most bluntly:
Open source is a licensing and delivery mechanism, period. It means you get the source for software and the right to use and modify it. All social impositions associated with it, including the idea of ‘community-driven-development’ are part of a recently-invented mythology with little basis in how things actually work […]
I’m not sure how widespread this view is. But it feels like in the world of software, and by extension to some extent in research software, people are more hostile to each other, with competing frameworks and solutions to a problem, claiming victory by domination: see the editor war of vim vs. Emacs, or Linux vs. the rest, or Python vs. Perl. And sometimes, even within the same community, disagreement becomes so great that people hard fork the project and part ways, as XEmacs did from GNU Emacs, and LibreOffice from OpenOffice.org.
Open source being something we don’t need to collaborate on is so fundamental to software engineers that the reaction to OpenAI dropping a Navier–Stokes blowup proof is alien to them. Here is an open source package, released under a license. If you use it, abide by it. There is no warranty, so buyer beware: the common open source licenses all disclaim one, as the MIT license does:
THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND […]
Thomas Depierre, a maintainer, draws the conclusion: “There is no supply chain here. Because there is no supplier.” (Depierre 2022)
Now OpenAI is doing the same thing with a special kind of software: a Lean program that compiles. And now everyone wants to claim a warranty.
P.S. To be very explicit, this is not to defend what OpenAI has done, as I have argued in Progressive disclosure for mathematical proofs. But it shows how different the two cultures are, each alien to the other. Mathematics happening to become a special kind of software forces these two cultures into an equilibrium with one another, and that is why it is so confusing and chaotic.