(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.
Do you buy stuff made in factories of do you open your wallet for everything handmade craft products? Or it's fine as long as craftsmen's jobs got replaced, just not when yours? Do you ever use a self-checkout? An ATM? Or do you pay extra to get cash from a human cashier at the bank?
Do you actually think this is a good argument? I had literally zero say in what happened in the past. I did not support the Midwest getting gutted. I wasn’t even able to vote when that was happening? Would it shock you that I generally think capital is misaligned to humanity?
> Would it shock you that I generally think capital is misaligned to humanity?
You still prefer to get cheaper options yourself. I know this argument gets caricatured in the "yet you participate in society" meme, but the point is that this is the aggregate result of individual humans making decisions on where to allocate their resources. You can attack this using various ideological and religious frameworks, but if it's just some stoner college freshman's communism, I'm not interested (neither if it's the more potent version that dispossessed my ancestors in Eastern Europe).
I don’t “prefer” to get cheaper options in any meaningful sense. There is no choice of mine involved in what products corporations serve. I have to buy the cheapest option because I have a poverty wage and have to survive.
The meaningful sense is when you open your wallet and buy one option when another option is there. Of course you have a budget and choose rationally, which is kinda like a forced choice. But you could always go and buy from the mom and pop shop and you could buy handmade clothes. Well, you don't have the money for it. Neither did people have it generations ago, they just wore worse clothes, went barefeet to school etc. You could still do that, walk barefoot until you can afford a handmade shoe and keep that for decades. It is in fact your preference not to do this, even if you want to claim that social pressure predetermines that you can't go around barefoot etc. At some point we disprove free will and agency entirely. Nobody in any historical era had more choice to express their preferences than consumers today.
I am not allowed to walk into my office without shoes. My shoes have had holes for 90% of my life. I assure you I own fewer things than you are imagining.
Also is your position really that nobody can point to problems or criticize anything without a fully fleshed political system to replace the USA with? I don’t support the excesses of the system of the USSR or 1950s-1980s China.
You can criticize things of course, like you can shake your fist at a cloud too when you'd rather want a sunny day, but the results may vary. You're asking people to refrain from using a cost-saving technology and instead spend more money on things that can be obtained easier with the tech. This means going against one's own rational interest. Such things usually happen willfully when the person believes in a religion like the Amish or Hasidic Jews. So having a fully fleshed political/ideological system on as similar level will be necessary here.
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 ↗
bonoboTP · · focus · HN ↗
GPerson · · focus · HN ↗
bonoboTP · · focus · HN ↗
You still prefer to get cheaper options yourself. I know this argument gets caricatured in the "yet you participate in society" meme, but the point is that this is the aggregate result of individual humans making decisions on where to allocate their resources. You can attack this using various ideological and religious frameworks, but if it's just some stoner college freshman's communism, I'm not interested (neither if it's the more potent version that dispossessed my ancestors in Eastern Europe).
GPerson · · focus · HN ↗
bonoboTP · · focus · HN ↗
GPerson · · focus · HN ↗
GPerson · · focus · HN ↗
bonoboTP · · focus · HN ↗