It's a truly wonderful read, made better by the fact the author doesn't quite understand what's going on.

The usual format that fun mathematics is presented (being talked at by someone who is very well versed in the subject) comes with a heavy cognitive burden - and often I just can't really make it through.

When the author is not an expert the writing is just so much more accessible - it's easier to understand and making it through feels more of an adventure and less of a lecture.

I've never thought previously how much I would enjoy this format though. I'm here to see more amateurs stumbling through mathematics.

Also, wasn't expecting this sort of side-quest from the guy who got me into React.

Heh, I like this. but it should be pointed out that from the other point of view, software developers were the supernatural beings (dare I say demons), which the sorcery of a good project manager could tame (with more or less success) to perform the desired magical effect

I’ve felt like a warlock for about half a year now - talking to demons which summon code from the abyss. Exhilarating and terrifying, especially when you can tell the demons get better faster.

> in which they themselves aren't quite able to validate whether the spell worked or not

Knowledge is of 2 kinds: know-that and know-how. Know-that is what LLMs are enabling such as the proof here, while know-how is more useful as that constitutes understanding and puts that knowledge to use.

The sorcerers have always outnumbered the wizards. Before AI, we called them code monkeys.

It's impossible for finite number of LLMs to solve all theorems. This would imply that the busy beaver sequence is computable which implies the halting problem is decidable.

For any finite program (eg some LLMs), there is a true math theorem which they cannot prove or disprove (given fixed input of the statement with no other information sources). If that weren’t true, BB would be computable.

Math is beyond computation. Since AI is just bits in bits out, it has this fundamental limitation.

Any magic of AI systems comes from the transformed meaning of its input data. With fixed weights any LLM is just an artifact. For example a human prompting an LLM constitutes an extra information source, which removes the above limitations. In theory any input from the natural world would remove the limitations too. The natural world is a black box and we don't know what kind of meaning or intelligence could underly it.

lol same with people.

"Given infinite thinking time a finite number of humans will solve all theorems"

I also love the angle that this was not intelligence just brute force. As if the mathematicians didn't reeaaally want to solve this they were just too lazy to give it a good try.

What does AI have to actually do before you realize these things are actually smart?

OP has reportedly been in contact with Prof. Mantova, who actually worked (jointly with S. L'Innocente) on the key human-authored results behind this AI proof and is arguably in the best position to understand exactly what the AI added that wasn't known before. (See the OP's thread on the Lean Zulip.) So this is happening, and we might see an actual paper publication of this result down the line (possibly encompassing multiple roughly self-contained papers, building up to the final result). The current AI-written version is way too obscure for that, and the AI-written human-targeted "summaries" are not really helpful. Again the OP is quite aware of this.

Hah, very interesting question!

Let me first clarify my relationship with mathematics. I think of myself as "an awestruck observer from a distance". I find some parts that I understand beautiful, and I have also tried to understand some of the basics rigorously. However, I generally just can't make my way through any serious paper, as I both lack the prerequisites and struggle with the amount of inference mathematics tends to place on the reader. That's the "from a distance" part.

Now, about picking the problem. I am genuinely "pulled by" surreal numbers themselves. I find them irresistibly beautiful. There is also a bit of bitterness around how they haven't fulfilled their promise (yet?) as Conway hoped they would be able to become a better foundation for some mathematics. But they are a bit too difficult to prove things about so far, and we know too little about them. So what "pulls me" also is a possibility of making enough dents in this that we would be able to use them more broadly, and learn even more things about them.

However, I do not know the details of the latest research. I don't know which problems have actually been solved, which pursue Conway's original vision vs narrower approaches, and which are elegant enough to feel "awestruck" enough about. So this is an invitation from me to LLM to share what it "feels pulled by" (for whatever definition; I think of it as just navigating the languagespace) , and then sifting through that list to see if something it lists makes me feel something. I would assume that with the field currently being so small (serious mathematicians mostly don't care about surreals), it's easy to get the LLM "excited" (again, just a vector in the languagespace) enough that it would give me genuinely interesting candidates. Then it's up to me to sift through them and see if they "speak" to me.

It's like asking a mathrock nerd to share their favorite mathrock albums. Niche enough that you'd likely get good results. Then you can listen and form an opinion.

In this particular example, the "ONAG birthday" and "maybe last Conway's unsolved conjecture about surreals" part spoke to me emotionally, the statement itself amazed me with its simplicity, and I felt "blood in the water" related to the recent results bringing the conjecture closer. So I felt the pull myself and went with it.

I use you, me, us interchangably because I don't think it really matters for anything and I don't need to reaffirm my individuality with such words.