(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.
The direction of continue shotting will develop a new culture that lead to a much more wider understanding for humans in the field of math. Find a way to accept this new culture and you'll thrive.
I apologize to GPerson for needlessly trying to convince him to my point of view. He seems to be an smart person deeply affected by how LLM are affecting his vocation and work. It was wrong of me to do this and I will take a break from this website for one week.
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 ↗
unified101 · · focus · HN ↗
GPerson · · focus · HN ↗
unified101 · · focus · HN ↗
GPerson · · focus · HN ↗
unified101 · · focus · HN ↗
GPerson · · focus · HN ↗
unified101 · · focus · HN ↗