19
long rant about math
The recent big AI results in math have left me in quite a bad mood. I believe the main ingredient is Lean, which is a formal language resembling a programming language. Math proofs written in Lean can be verified deterministically with a computer, which really helps mitigate the hallucination problems of LLMs. Back in the days of pure scaling LLMs and Sam Altman talking about Dyson spheres, I was skeptical that LLMs would do math, but I did think that perhaps in the future, techniques using these formal languages could contribute to math. Well, it seems like OpenAI and Anthropic had the same idea and I underestimated their limitless checkbooks. Many of the biggest results were announced by mathematicians directly working for them (and presumably being paid a handsome amount).
For what it's worth, after the last of these big announcements, I decided to try one of these AIs on one of my small problems that I couldn't figure out. The AI did give a solution. That is, until I checked it thoroughly and realized that the it had a subtle but severe mistake that made it useless. I reprompted it, it failed again, and I ran out of tokens. I'm sure someone will tell me to shell out $200/mo for a pro subscription.
In the math and computer science research community, this is all anyone can really talk about right now. Honestly, after watching this whole AI bubble starting from the very beginning, I think the AI companies want to use marketing to stoke fear that all mathematicians will be replaced. But now, I am just too tired to argue. The amount of alarm and the extraordinary social pressure to use LLMs has soured me to this whole research thing. If becoming a researcher will one day require supporting these evil AI companies, I would rather just not. My dream job now is Factorio developer.
A lot of annoying people in technical areas view the world in terms of an intelligence hierarchy: the smartest people do math and physics, the slightly less smart people do coding, and the dumb people do everything else. So if AI can do math then it can do anything else. But, as an example, it is abundantly obvious now that AI is not replacing filmmaking. The techbros might be moved by arguments about how hilariously expensive video generation is, and how all these videos are 2 second clips stitched together so you won't feel the uncanny valley. But the real reason is that nobody wants to watch slop made with no intention or feeling. Also, nobody wants to support the AI companies, which could not act more evil even if they tried.
The mania in math right now quite resembles the mania in software engineering back in December-February, when Claude Code definitely solved all coding. I don't think the boosters expected that by April, everyone would be complaining about how expensive it all was while seeing an endless parade of vibe coding disasters (and no increase in productivity). Even if math research works out perfectly well (which is a still big if), it's not going to pay the bills. They would need to find a use case in the real world, where hallucinations can cause serious damage and cannot be formally prevented. And they have certainly tried. Math will not change the fact that all of this will collapse.
