I don't understand what you are trying to say. Which of the following is it, (or is it something else entirely)? 1. There is a much shorter proof that would al

I don't understand what you are trying to say. Which of the following is it, (or is it something else entirely)? 1. There is a much shorter proof that would also be accepted by lean, we just aren't thinking about the problems in the right way so we can't find it. On one level this is obviously true, Anthropic did not put any effort in to minimising the length of the proof during its development or afterwards. 2. There is a much shorter proof if we took different axioms instead of the ones built into lean. I find this much harder to believe, unless your new axiom is basically just FLT. Otherwise all reasonable axioms are not too hard to show as equivalent to each other (in terms of what they prove in PA anyway), so such an equivalence proof would be a small portion of the 13 million lines of lean.