(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.
I appreciate the sentiment, especially after the escalation of the last few weeks. But I am hoping this story can become an example of why mathematicians are still very much needed and LLMs are still severely lacking when it comes to displacing scientists. Conway's conjecture has no application whatsoever, even within pure maths, and the only point in pursuing it is what you can learn in the process, and whether you can make something beautiful. LLMs are consistently unable to do the latter (and yes, some mathematicians are also not very good at it... this is an old topic of discussion, just amplified by current events). To me it feels like the technology is still where it was in 2015 when DeepDream images came out: increasingly good at pattern matching, but still a lot more like dreaming than thinking. So our job is still there somewhere.
The problem is rather how quickly we can change our ways of working to make sure the training and hiring pipeline does not collapse. That's the disastrous scenario, for both the individuals affected and the discipline, that we must avert somehow. I wish we had an easy answer to that. I certainly don't. But I like to think that at least engaging with the public in a constructive way will have a net positive effect.
I’m not actually upset with your actions I was just worked up at the time. You’re in a dilemma and graciously handling it the way you are is the only sensible path.
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 ↗
xworld21 · · focus · HN ↗
The problem is rather how quickly we can change our ways of working to make sure the training and hiring pipeline does not collapse. That's the disastrous scenario, for both the individuals affected and the discipline, that we must avert somehow. I wish we had an easy answer to that. I certainly don't. But I like to think that at least engaging with the public in a constructive way will have a net positive effect.
GPerson · · focus · HN ↗