Do you have any philosophical guesses regarding why on Earth this problem has turned out to be so cursed? Why does there appear to be no “common-sensical” proof? Usually that’d be either because (a) there’s some missing intermediate theory (in whose language the proof would be short and elegant) or (b) the conjecture itself is “unnatural”/”ad-hoc” in some sense (such that it would only be compactly provable in terms of similarly ad-hoc frameworks). Does either of those seem like the right diagnosis? If (a), it might be worth studying the proof for hints of the concepts/abstractions this missing theory is using, the knowledge of which may make subsequent work in the neighbourhood easier. If (b), there may be hints regarding what a more “natural” conjecture would look like. (Of course, it may be neither.)
Has there been any progress on redunds, either formal or conceptual (e. g., rephrasing the conjecture that you’re attempting to prove)?
No idea. I hope to have a simpler proof soon and hopefully that simpler proof will reveal some nice insights about this “cursed” problem. Heck, it could be the current proof already does that, I haven’t gone over its internals all that carefully (both a cost and selling point of formalizing this in lean.)
Awesome/this is a relief.
Do you have any philosophical guesses regarding why on Earth this problem has turned out to be so cursed? Why does there appear to be no “common-sensical” proof? Usually that’d be either because (a) there’s some missing intermediate theory (in whose language the proof would be short and elegant) or (b) the conjecture itself is “unnatural”/”ad-hoc” in some sense (such that it would only be compactly provable in terms of similarly ad-hoc frameworks). Does either of those seem like the right diagnosis? If (a), it might be worth studying the proof for hints of the concepts/abstractions this missing theory is using, the knowledge of which may make subsequent work in the neighbourhood easier. If (b), there may be hints regarding what a more “natural” conjecture would look like. (Of course, it may be neither.)
Has there been any progress on redunds, either formal or conceptual (e. g., rephrasing the conjecture that you’re attempting to prove)?
No idea. I hope to have a simpler proof soon and hopefully that simpler proof will reveal some nice insights about this “cursed” problem. Heck, it could be the current proof already does that, I haven’t gone over its internals all that carefully (both a cost and selling point of formalizing this in lean.)