4 ms·

(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 und

(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. Good luck!

zozbot234 15d ago
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.
- xworld21 15d ago
  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.
  - GPerson 14d ago
    Thanks for encouraging the end of our career.
    - zozbot234 14d ago
      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.)
      - GPerson 14d ago
        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.
        zozbot234 14d ago
        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.
        GPerson 14d ago

zozbot234 15d ago

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.

xworld21 15d ago
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.
- GPerson 14d ago
  Thanks for encouraging the end of our career.
  - zozbot234 14d ago
    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.)
    - GPerson 14d ago
      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.
      - zozbot234 14d ago
        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.
        GPerson 14d ago