(Background: trained, published, but still amateur mathematician.)
This is a cool blog post and I think you're going the right way, and beginning to get an understanding of the proof as you go.
I'd recommend continuing on the simplification and understanding route, until you yourself can follow the proof. Some suggestions, as I did something similar:
1. See if (or ask the AIs) if individual parts of the proof can be found elsewhere, i.e., is an argument just a copy of something else? If so, it's important to attribute this, but also this usually allows simplification ("by Theorem X", etc.)
2. Look for redundant patterns and try to combine them.
3. Ask the AI to be a critical reviewer from some journal, and try to fix its criticisms.
4. Continue simplifying! Assume that the final result may actually be relatively short.
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.
Vincenzo (Mantova) here: yes, I have been reading bits and pieces of the proof and I can say for sure that the method is sound, at least for the first half (power series with real exponents). I haven't even tried reading the part that mentions the Cantor-Bendixson rank yet, although given how the rest went, I'd be really surprised if there's a problem there.
As with most interesting proofs, the number of core ideas is actually small, I'd say two for the real exponents, and presumably a third idea for lifting up to omnific integers. I have been redoing the real exponents part of the proof going on the ideas only, and with a few smarter choices, I am converging on something very short. And I mean very short, which is amazing. I didn't think the answer would be this close: it 'just' needs looking at the problem from the right angle, and also make a fairly bold guess at the outcome.
Dan's current proof is of course much longer. Between the fossilized ideas that Dan mentions in the post and the formalisation of previous results, there's a lot of cruft that inflates the proof but does not really help understanding what is going on. Luckily the word 'derivation' pops up early, otherwise it would have been very challenging to wade through the lemmas to find the important points.
Nope I’m airing them right here. This guy didn’t do any work except tell the bot to continue for a month. That’s not work, that’s just unhealthy and negative. He’s made no intellectual progress. He doesn’t even know any mathematics and has never cared to learn. He’s just lucky other people are there and kind enough to let him dump his slop onto. They could have done this and gotten a lot more out of it.
You can definitely argue that the user's direction and curation work was intellectually trivial (though there's meaningful room for disagreement even there, especially wrt. having the AI stick to established terminology/broad approaches - this is arguably a sort of successful "systematizing" work, though only in a very minimal sense) but this was not a one-shotted result. The blog post is extremely clear about that.
And of course, going by their own admission, they couldn't "have done this themselves": the most you can argue wrt. this is that Mantova and L'Innocente, or some other narrow domain experts, might have done this themselves and that AI "scooped" this result from them.
Nobody said it was one-shotted? It was mindlessly “continue-shotted” except for the brilliant idea of upgrading the model. Obviously the models are going to be improved to the point where typing continue continue, how ya feeling, continue continue, okay let’s double check this, upgrade model, continue continue, will be less necessary.
I was not "mindlessly continue-shotting". The way you describe it is literally the same as "one-shotting" and, as I explained in the article, it simply doesn't work. You are welcome to try it yourself on this problem to verify that.
Yes, I was not doing any mathematical work in curating the output, but the article makes it quite clear that pivots and constraints the LLM would not impose on itself were critical to actually making progress.
Also:
>He doesn’t even know any mathematics and has never cared to learn
While I don't know enough mathematics to work on this problem, claiming something like this is preposterous. As I link in the first paragraph of the article, I've been learning mathematics on my own by going through Terence Tao's Analysis book and solving exercises. I'm familiar with the concepts of mathematical definitions, proofs, etc. I've gotten about halfway through the book solving them on paper before abandoning it (and later got through the first few chapters in Lean, also solving every exercise — by hand, mind you). Sure, this doesn't make me a mathematician, but I'm closer to a dropout first-year student than to someone who has "never cared to learn".
You’re a guy who benefited from easy choices which led to you a life of luxury and now you use your high perch to shit on people who were stupid enough to work hard to do something more meaningful with their lives than attain wealth and social status.
Edit I apologize to Dan Abramov for venting my frustrations about things outside of either of our control and unfairly using him as a punching bag. He seems to be an intelligent person and I hope he continues learning mathematics using whatever tools he sees fit, including AI. It was wrong of me to do this and I will take a break from this website for one week. I won’t hide this comment though it is shameful.
pretzellogician · · focus · HN ↗
This is a cool blog post and I think you're going the right way, and beginning to get an understanding of the proof as you go.
I'd recommend continuing on the simplification and understanding route, until you yourself can follow the proof. Some suggestions, as I did something similar:
1. See if (or ask the AIs) if individual parts of the proof can be found elsewhere, i.e., is an argument just a copy of something else? If so, it's important to attribute this, but also this usually allows simplification ("by Theorem X", etc.)
2. Look for redundant patterns and try to combine them.
3. Ask the AI to be a critical reviewer from some journal, and try to fix its criticisms.
4. Continue simplifying! Assume that the final result may actually be relatively short.
Good luck!
zozbot234 · · focus · HN ↗
xworld21 · · focus · HN ↗
As with most interesting proofs, the number of core ideas is actually small, I'd say two for the real exponents, and presumably a third idea for lifting up to omnific integers. I have been redoing the real exponents part of the proof going on the ideas only, and with a few smarter choices, I am converging on something very short. And I mean very short, which is amazing. I didn't think the answer would be this close: it 'just' needs looking at the problem from the right angle, and also make a fairly bold guess at the outcome.
Dan's current proof is of course much longer. Between the fossilized ideas that Dan mentions in the post and the formalisation of previous results, there's a lot of cruft that inflates the proof but does not really help understanding what is going on. Luckily the word 'derivation' pops up early, otherwise it would have been very challenging to wade through the lemmas to find the important points.
GPerson · · focus · HN ↗
unified101 · · focus · HN ↗
Air your LLM greviences someplace else.
GPerson · · focus · HN ↗
zozbot234 · · focus · HN ↗
And of course, going by their own admission, they couldn't "have done this themselves": the most you can argue wrt. this is that Mantova and L'Innocente, or some other narrow domain experts, might have done this themselves and that AI "scooped" this result from them.
GPerson · · focus · HN ↗
danabramov · · focus · HN ↗
Yes, I was not doing any mathematical work in curating the output, but the article makes it quite clear that pivots and constraints the LLM would not impose on itself were critical to actually making progress.
Also:
>He doesn’t even know any mathematics and has never cared to learn
While I don't know enough mathematics to work on this problem, claiming something like this is preposterous. As I link in the first paragraph of the article, I've been learning mathematics on my own by going through Terence Tao's Analysis book and solving exercises. I'm familiar with the concepts of mathematical definitions, proofs, etc. I've gotten about halfway through the book solving them on paper before abandoning it (and later got through the first few chapters in Lean, also solving every exercise — by hand, mind you). Sure, this doesn't make me a mathematician, but I'm closer to a dropout first-year student than to someone who has "never cared to learn".
GPerson · · focus · HN ↗
Edit I apologize to Dan Abramov for venting my frustrations about things outside of either of our control and unfairly using him as a punching bag. He seems to be an intelligent person and I hope he continues learning mathematics using whatever tools he sees fit, including AI. It was wrong of me to do this and I will take a break from this website for one week. I won’t hide this comment though it is shameful.