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.

If anything, I'd treat him as a table of contents to things other people do.

The whole world has always been like this. It's just showing up with force here.

Comments URL: https://news.ycombinator.com/item?id=50165822

Points: 3

# Comments: 0

There are suddenly many new solutions to problems that have resisted sustained attacks (e.g. the Uniform Games Conjecture as detailed in TFA at some length). Where do you think they are coming from? Why is there suddenly a bunch of results to be stolen?

(That said, this is not fun, and I sympathise! I'm still a student and would like to avoid finance if at all possible. Just suggesting not to drop everything if you feel like you're learning in the process.)

(I'm now personally in the position of having to choose a PhD project, and this rapid change is interacting with making long-term plans really badly. Guidance welcome!)

Already the unit distance proof was substantially human-edited (per Thomas Bloom). Then with the ten problems from Astra you started getting the citation issues. Then Navier-Stokes was a rushed 160 pages with barely any citations, and some of the related papers were called (by their "authors") the ugliest mess they've ever seen.

And now here we are. At least it seems that mathematical ability and communication with a mathematical audience are independent skills, and progress in the first does not imply the second.

This doesn't surprise me much, given two analogies: 1) many smart people are nonetheless horrible lecturers. (You can't quite get the opposite extreme, since to explain math well you have to be able to do it.) 2) AI writing in general hasn't improved. The models have annoying verbal tics ("honestly") and have no sense of which part of what they say is obvious and which is relevant.

Also, it still seems that AI has a much different style from humans, with more brute force and using obscure literature results, and the future might still end up human/AI complementary. We aren't in an AlphaZero situation where the AI learns everything through self-play. (Yet? But we don't even seem to be moving that way much? Can anybody qualified help out?) Things are just moving really fast now and it's hard to process everything.

In looking at this over the past hour, I haven't seen clear evidence one way or the other. Some of the stuff is highly unexpected (like the multiplication algorithm), but counterexample-y, and about the rest the professional mathematicians online seem to have a consensus that it's not "breaking through fundamental obstacles". I suspect neither of us is competent to judge that.

Math is incredibly rich, and even the simplest things have insanely complicated structure when you zoom in. However this all ends up, math is bigger than LLMs, and the people who claim it is getting "solved" and we are running out of open problems haven't stared into the abyss enough.

One thing I noticed was that more than a few were seriously sick in childhood and had to be homeschooled. This includes Edward Morley, Peter Higgs, René Descartes (though I'm not sure how rare it was at his time), and the mathematician Julia Robinson, who was bedridden with scarlet fever at 9 years old, then had to get tutoring to catch back up, and had this to say about it [2]:

> I have since read that a solitary childhood or, what amounts to the same thing, a period of isolation resulting from an illness is frequently noted in the early lives of scientists. I am not sure what the significance of this finding is. Obviously I had to amuse myself for long periods of time, but I didn’t do so with mathematics. I am inclined to think that what I learned during that year in bed was patience.

> By the time I was well enough to go back to school, I had missed more than two years. My parents arranged to have me tutored by a retired elementary school teacher. In one year, working three mornings a week, she and I went through the state syllabuses for the fifth, sixth, seventh, and eighth grades. It makes me wonder how much time must be wasted in classrooms.

Sidenote: I found the book [1] through asking a free LLM what source this quote might be referring to. They are reasonably good at this kind of literature search, especially because it's easy to judge whether they gave you something useful.

[1] https://archive.org/details/cradlesofeminenc0000goer_l9f8/pa...

[2] https://web.archive.org/web/20181207045746/https://www.maa.o...

Conversations with strangers can be hard to get going, but they aren't this bad.

Q: do you like doing psych studies and why?

A: theyre chill, easy money tbh

Q: yeah same. Could you give me an easy cupcake recipe off the top of your head?

A: nah i just get the box mix lol

Q: haha fair enough, i couldn't either. Last question, what's your favorite weird animal?

A: axolotl, theyre weirdly cute

And that's the whole thing. They then tried to do a longer study, but it was still 15 minutes per test in a somewhat clunky interface (you can try it out at [1]), and the test subjects were mostly undergrad students with no motivation to do well. Less than half tried any sort of trick question. ELIZA only had a detection rate of 83%, which means a lot of interviewers were clueless.

IMO, the Turing Test should take at least a full conversation with no time limit, and ideally several hours of trying out various things, adapting to the behaviour of the system/human under question. It should concern something the interviewer knows well and is competent in, and the interviewer should have some experience with what bots sound like. (Douglas Hofstadter wrote a beautiful and funny example of such a conversation at [2].) Only then do you have some idea how adversarially robust the system is. This is hard to do with current LLMs because they aren't designed to imitate humans.

[0]: https://arxiv.org/pdf/2503.23674 (now published at https://www.pnas.org/doi/epdf/10.1073/pnas.2524472123). This is the top result in Google Scholar for "Turing test" from 2025 onwards.

[1]: https://turingtest.live/

[2]: "Dull Rigid Human meets Ace Mechanical Translator" (https://www.cambridge.org/core/books/abs/once-and-future-tur... or alternative access methods thereof)