Comment by morpheos137 | Hacker News Reader

Comment by morpheos137 | Hacker News Reader

Parent Full thread

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.

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.

https://en.wikipedia.org/wiki/Proof_theory is pretty much about this.

What is that shorter proof and how does it work? Is there a layman-accessible version?

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.

Reply on news.ycombinator.com