6 ms·

Mine is much shorter though...

morpheos137 11d ago
There is a shorter proof but since thinking ossified in the 20th century we won't be sociologicaly ready to accept it at this time. Much of math is playing according to arbitrary culturally enforced rules that are not natural in the sense of being minimum logical requirements. Take the axiom of infinity or the axiom of choice for example. Fundamental math need not be based on zfc but that is what we have chosen as our foundation because we elevated continuity, infinity to ontological higher status than distinguishability. In the past similar cultural barriers were present in math for example imaginary numbers are so called because the name originated as derision. It seems unlikely to suggest that math today is not similarly culturally constrained in certain areas and some things we find confounding are more so due to our choice of foundation than their intrinsic nature.
- perching_aix 11d ago
  What is that shorter proof and how does it work? Is there a layman-accessible version?
  - morpheos137 11d ago
    Someday. It is has to do with degrees of freedom and information encoding in terms. Stop assuming operations are external but consider them as relational degrees of freedom of a logical statement. Different complexity statements can support different complexity results.
- sebzim4500 11d ago
  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.
- RGamma 11d ago
  https://en.wikipedia.org/wiki/Proof_theory https://en.wikipedia.org/wiki/Proof_theory is pretty much about this.

There is a shorter proof but since thinking ossified in the 20th century we won't be sociologicaly ready to accept it at this time. Much of math is playing according to arbitrary culturally enforced rules that are not natural in the sense of being minimum logical requirements. Take the axiom of infinity or the axiom of choice for example. Fundamental math need not be based on zfc but that is what we have chosen as our foundation because we elevated continuity, infinity to ontological higher status than distinguishability. In the past similar cultural barriers were present in math for example imaginary numbers are so called because the name originated as derision. It seems unlikely to suggest that math today is not similarly culturally constrained in certain areas and some things we find confounding are more so due to our choice of foundation than their intrinsic nature.

perching_aix 11d ago
What is that shorter proof and how does it work? Is there a layman-accessible version?
- morpheos137 11d ago
  Someday. It is has to do with degrees of freedom and information encoding in terms. Stop assuming operations are external but consider them as relational degrees of freedom of a logical statement. Different complexity statements can support different complexity results.
sebzim4500 11d ago
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.
RGamma 11d ago
https://en.wikipedia.org/wiki/Proof_theory https://en.wikipedia.org/wiki/Proof_theory is pretty much about this.