(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.
Needless to say, I disagree that what Prof. Mantova is planning to do (digesting the proof and making it human-understandable) represents the "end of [mathematicians'] career". Systematizing has always been a key part of human mathematical work, and tidying up a raw proof can be viewed as a kind of systematizing.
My hope is also that Mantova and very possibly L'Innocente will get a substantial share of credit for their role in the resolution of this conjecture by Conway: the AI would not have embarked on this were it not for their prior work. So even human mathematicians with an inclination for more exploratory "problem solving" will have plenty to do in the future. (The story is actually not that different for the recent Navier-Stokes forced blowup result, which also built on key conceptual work from 2023 by Córdoba and Martinez-Zoroa.)
Luckily for these guys the problem is famous enough that giving some kind of credit for its resolution even makes sense at all. The vast majority of published work is not like this. There’s not going to be any credit divvied up to the thousands of people who’s work was probably involved in the recent formalization of FLT, which involved formalizing 300 thousand theorems.
Kevin Buzzard has reportedly been working on a more systematized (i.e. leveraging a more modern approach) and human-targeted formalization of FLT. I certainly hope that his work continues and he gets the deserved credit. Of course there is also some possibility that it won't, and that would mean you have a point after all.
You’re just mentioning established and famous people. What about the average people who are just going to get fucked for spending their lives trying to promote humanity, just to be rewarded with the risk of economic ruin and no job prospects?
If Mantova and L'Innocente (as well as Córdoba and Martinez-Zoroa) count as "famous people" now, I would say that their fame is quite deserved! Would you disagree that AI played a significant part in surfacing their work? Aside from that, I'm not really sure what to make of your comment. I do sympathize for the researchers who are at risk of having their ongoing work "scooped" by AI (and for all we know, this may even include Mantova and L'Innocente) but the way to address that is to still have "divying up" of relevant human credit.
I'm not working on some famous conjecture, just following my curiosity, and I think I found something (minor and specific) that should reignite a young mathematician's interest for work she did almost a decade ago, for a phd she never used (she left academia). I'm going to have flowers delivered to her, with a brief note explaining what I think I found and encouragement to resume her academic career and reach out to a her former co-authors.
Keep doing things that people want to pay for. If this becomes impossible, the world will face a much broader political crisis than "mathematics careers". How concerned were you when manufacturing industries died in certain regions and jobs got wiped out? Or it only matters when it's academics?
It shows that the issue is much broader and myopically focusing on how math PhD students will be evaluated etc. entirely misses the forest for the trees, it's just not even close in proportionality.
This is indeed also coming for law, medicine, and banking, though licensed professions will hold out for longer because you need someone to put in jail when things go wrong. The problem is that all this is extremely over politicized and nobody is able to think clearly. They want to simultaneously say all this is just hype and a bubble and will go away like NFTs did, and also are starting to worry about economic replacement. Some more coherent political narrative will have to be formed.
I’ll state this again. How does my economic redundancy get mitigated in anyway by being the first on the chopping block by several years? Do you think being jobless for 3 years is just missing the forest for the trees?
Since it will be coming for everyone, the solution will be major social upheaval with some consequence for all of humanity, hopefully a good one where we somehow manage to keep on living some kind of good life.
Regarding being jobless for the 3 intervening years, it is certainly a personal concern but in this temporary phase there are still some other jobs for smart people. Once there aren't any, we are entering the part that I was talking about where you will be far from alone and you can join together to exert some kind of political pressure but it will not be about math PhDs, but employment as a whole. And it may not be very effective if AI is on the other side, not on yours. Yeah, it sounds like scifi, and people want to dismiss scifi concerns and instead focus just one inch ahead of their toes, instead of seeing the writing on the wall.
For some reason you think I’m opposed to the use of AI in mathematics. This is not the case. If this guy sat down to actually learn the math and then did actual work to disseminate the knowledge in a positive sustainable way it would be a different story. His actions are just here to inspire more people to use this tool in counterproductive ways.
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 ↗
zozbot234 · · focus · HN ↗
My hope is also that Mantova and very possibly L'Innocente will get a substantial share of credit for their role in the resolution of this conjecture by Conway: the AI would not have embarked on this were it not for their prior work. So even human mathematicians with an inclination for more exploratory "problem solving" will have plenty to do in the future. (The story is actually not that different for the recent Navier-Stokes forced blowup result, which also built on key conceptual work from 2023 by Córdoba and Martinez-Zoroa.)
GPerson · · focus · HN ↗
zozbot234 · · focus · HN ↗
GPerson · · focus · HN ↗
zozbot234 · · focus · HN ↗
GPerson · · focus · HN ↗
Xmd5a · · focus · HN ↗
bonoboTP · · focus · HN ↗
GPerson · · focus · HN ↗
The math career is going to killed off 2-3 years before law and medicine and Wall Street banker. How does this make me more secure in any way?
bonoboTP · · focus · HN ↗
This is indeed also coming for law, medicine, and banking, though licensed professions will hold out for longer because you need someone to put in jail when things go wrong. The problem is that all this is extremely over politicized and nobody is able to think clearly. They want to simultaneously say all this is just hype and a bubble and will go away like NFTs did, and also are starting to worry about economic replacement. Some more coherent political narrative will have to be formed.
GPerson · · focus · HN ↗
bonoboTP · · focus · HN ↗
Regarding being jobless for the 3 intervening years, it is certainly a personal concern but in this temporary phase there are still some other jobs for smart people. Once there aren't any, we are entering the part that I was talking about where you will be far from alone and you can join together to exert some kind of political pressure but it will not be about math PhDs, but employment as a whole. And it may not be very effective if AI is on the other side, not on yours. Yeah, it sounds like scifi, and people want to dismiss scifi concerns and instead focus just one inch ahead of their toes, instead of seeing the writing on the wall.
GPerson · · focus · HN ↗