Comment by 0c3ca83
18 hours ago
That's like saying "you love cooking, so for fast progress you insert coins into doordash to make fast progress on a meal". If you do that, you don't love cooking.
It's fundamentally incongruous with someone that "loves the game". And I hope that you have a good excuse for ruining it, hopefully a seven or eight figure excuse.
> That's like saying "you love cooking, so for fast progress you insert coins into doordash to make fast progress on a meal". If you do that, you don't love cooking.
Rather, it's like saying "I love eating good food."
One approach is to learn to cook excellently, buy high-quality ingredients etc. Then invest time to cook a delicious meal. This is like learning math, becoming exceptional in one area, and then work on the problem.
Another approach is to go to a well-rated restaurant, order some food there, and pay a decent amount of money for the food. This is like buying AI tokens, and setting up some agents to work on math problems.
Both approaches are suitable. And I guess/hope many people who really would love to contribute to progress in mathematics would really prefer to go the first way. But because
- they are not highly gifted
- have a time-consuming daily job and/or family
- simply cannot afford the high opportunity cost to get to a suitable level in math
- ...
the only way such people can contribute to progress in math is the second approach. That's why these people behave like they do.
I am quite confident that most of such contributors don't like that their money lands in the hands of OpenAI/Anthropic.
So: Which approach would you recommend these people who are really eager to contribute to progress on some mathematical problems?
So, what's the game you claim to love? Wading through piles of poorly written proof and trying to de-slop it?
It's like saying "look, they may not be good at painting, so what can we do other than letting them take a can of spray paint to the contents of the Louvre?"
If you can't contribute, enjoy it passively, instead of doing damage.
(not GP)
Coming back to the particular project at the top of this thread (not TFA but the top comment), I don't see a problem with contributing to Lean verifications. One of the problems with the OpenAI dump is that half of it might be wrong, and formalizations resolve that. This is particularly relevant for this result, which is one of the few claims that didn't go in the direction one would expect before the drop.
You can for sure criticize OpenAI for not having done it themselves (I hereby do!). I guess you could make a case that engaging with their results somehow legitimizes their actions, but a) I don't expect OpenAI to care about this enough for it to matter, and b) you aren't making this case but a stronger one that any engagement somehow ruins mathematics and must be done for money. I don't think so! [1]
I personally am a complete amateur, but find this result one of the few overwhelmingly positive aspects of the drop. It's something people weren't expecting, so it probably saves time that would have been spent on trying to prove the O(n log n) lower bound; it's about a question that is extremely natural ("how fast can you multiply really big numbers", that's like the eight-year-old's vision of what math is!) and shows that there is absurdly complicated structure even behind the simplest things, which is why math is not getting "solved"; it didn't kill the question but started a whole program of trying to optimize the algorithm (currently AI-assisted, but I hope that if all AI magically disappeared tomorrow, in a few years people would be able to get there unassisted), plus TFA lists several other problems this algorithm could help with at the end of section 4.
That's the game I love, at least.
[1]: This was best put by Nestor Guillen (https://terrytao.wordpress.com/2026/09/13/happy-those-able-t...): AI with all its drama (of economic and political origin) is separate from LLMs the technology, which only work because they build on a corpus of intelligent text, including a lot of math. Had it been made by a responsible organization, and had it appeared more gradually, it could be treated as an amazing tool for literature search and testing how far a brute-force approach can go, which would only help test the value of new ideas. There is some shard of this in our actual situation as well, beneath all the politics.