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.
Not really appropriate for a HN comment but information theory holds the key. Diophantine equations are about doing certain atomic operations on integers. The argument is that at or above degree three exponentiation logical distinguishability of operation results becomes ambiguous thus no integer result is possible. Too many degrees of freedom to yield an in band result, kind of like how you can't have a knot in greater than 3 space. A logical closure requirement forces a^n + b^n = c only works with a, b, c, n integers for n < 3. Sketch: a + b is composition, = is identity, n=1 reduces to composition, n=2 is exponentiation but in degree 2. Exponentiation is iterated multiplication. The index of iteration and the number of terms is identical so they can share an operation. So the channels you must track are (1) what and how many parts are composed and how (addition of a and b terms), (2) are they identical to c, (3) what operation precedes composition of the lhs terms (multiplication, twice). Thus in case n=1 we have index two terms equal to 1 term on the right, c. The atomic logical operations are composition and identity: two degrees of freedom used integer result permitted. In case n=2 the atomic operations are composition, identity, exponentiation (multiplication of an identity by an index) so exponentiatiation reduces to indicibality. Three operations are used on three integer terms and it works. At and beyond n=3 your indicibality exceeds your term count so there must be a fourth or greater atomic operation so you need to count identity, composition (addition), exponentiation index and term count as distinct degrees of freedom. Fundamentally the number of distinct irreducible operations on terms can not exceed the term count and yield an integer result if you force the terms themselves to encode the operations. In other words mathematical operations are seen as relational degrees of freedom. The more atoms you have (terms) the more complex relations (operations) you can have. If you restrict yourself to two lhs terms then you can support no more than three irreducible operations however you label them: in the binary sense your options are 00 no op c=0, 01 c=2 a^0 + b^0 op count terms return result, 10 a^1 + b^1 = c sum terms, identify terms to get contingent result (operations 2, sum, compare or evaluate). 11 a^2 + b^2 = c multiply each term by itself the number of the term count (2, square then), sum, compare three distinct operations. The state of the system is determined by the binary present or absence of a quality. No terms no result 0=0 true. Terms with one operation exponentiation by n=0 yielding constant result 2, single op is count the terms assign value to c. Terms with two ops sum the terms assign value to c. Terms with three ops count the terms, self multiply by the count, assign value to c. Terms n=3 or greater require more ops than there are terms to describe them so identity of lhs to rhs must break. Thus fermats last theory is like asking why you can't have a triangle with more than three sides. The number of ops a system can admit at input and maintain logical closure (self adressibility) scales with the degrees of freedom of the output and the number of input and output terms. Thus if n is three or greater c must be more complex than an integer. Kind of non rigorous argument but that's the line of thought.
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.
I wonder if any piece of the lean code is in a shape which means it could be contributed to one of the existing Lean libraries.
My experience is that it takes a lot of human input to make Fable write code nice enough for a formalisation library others can work on. But since this is certainly a lot of prerequisites formalised as well, it would be nice if not all of the effort was wasted on one capstone proof!
(Repost of a earlier comment, but I feel it fits better here)
My anecdotal experience is that while LLMs are quite good at closing theorems given an LSP to inspect the proof-tree, they suffer from similar kind of problems with proofs as they do with bigger codebases in any language -- finding reusable parts that can be built into libraries (that's lemmas in Lean 4 sense). However, Buzzard has many times said that he wouldn't care how big the proof is and how ugly it would be, as long as there would be a proof.
I believe Lean supports a signature search mechanism. E.g. Haskell has Hoogle, Lean has Loogle. So in many ways it's actually easier to search for "library" code than in most languages, because the type tells you everything you need to know and you don't need to care about the implementation.
Serious question: how do you prove that the Lean interpreter itself (not to mention the toolchain built around it) is error-free? Isn't this turtles all the way down to some degree?
You can’t, so you keep the kernel small. The Lean tactics language is rich, so users can autogenerate proofs for the truly trivial bits, but the core language is checkable in dependent type theory.
Kernel bugs, like compiler bugs, exist. As of now, a prover is considered good if it has no known bugs that would thwart a mathematician working in good faith. It’s not considered responsible yet for being impervious to adverse users, but that may change in the age of Ai.
Metamath is short, which does make it easier to verify. In addition, because it's simple, there are many implementions. The set.mm Metamath database, the most popular, is checked by 5 independently implemented proof verifiers.
You haven't thought that through. The regress obviously isn't infinite, and it bottoms out in things that are immediately true by inspection. And seriously, how likely is it that you have stumbled upon a fundamental problem with the whole notion of automated proof that no one in the field has thought of?
I think an interesting problem, perhaps even more interesting problem, would be the shortest / most concise / easiest to understand (formally verifiably) proof.
Much of the value of proof is in the development of math definitions and intermediate theorems needed to get you there, Grothendiek-style. This ability seems still to be beyond AI (at least, I haven’t heard of any fundamentally new and useful definitions such as “scheme” or “modular form” emerging from the latest blizzard of AI proofs). BUT, I wonder if AI could develop this skill too through a process of efficiently refactoring a big Lean proof into Lean pieces, then interpreting the pieces back into new, human-grokable definitions with evocative names?
31 comments
[ 0.21 ms ] story [ 20.3 ms ] thread1. 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.
My experience is that it takes a lot of human input to make Fable write code nice enough for a formalisation library others can work on. But since this is certainly a lot of prerequisites formalised as well, it would be nice if not all of the effort was wasted on one capstone proof! (Repost of a earlier comment, but I feel it fits better here)
Lean is called that because the hope is the part that has to be correct by inspection ("the kernel") is small or "lean".
The kernel does have bugs sometimes.
Kernel bugs, like compiler bugs, exist. As of now, a prover is considered good if it has no known bugs that would thwart a mathematician working in good faith. It’s not considered responsible yet for being impervious to adverse users, but that may change in the age of Ai.
https://arxiv.org/html/2403.14064v3
https://github.com/digama0/lean4lean/tree/master
https://github.com/anthropics/fermats-last-theorem/blob/main...