I think the same happens now with AI generating code. Nobody will read every line. that's part of the process from now on.
fhdkweig
The problem of the proof was that we knew that FCT was true, but we had no idea why. A good/elegant proof teaches us something new about how that problem is related to other problems. It isn't just about getting a true/false answer to the conjecture.
layer8
I didn’t know we had invented time machines yet. ;)
jjtheblunt
the title made me think of a much older machine that was used for calculating https://en.wikipedia.org/wiki/Antikythera_mechanism
jmount
I think a lot of great ideas like tree-width were developed in hope of simplifying the proof.
DonHopkins
>[...] mogged [...] Ixnay on the celinay ingolay.
Animats
That takes me back to an early 1980s incident where I was criticized for an early computer-generated proof. This was when I was building a program verifier at an aerospace company. We had the first SAT solver, the Oppen-Nelson simplifier, and the first constructive theorem prover, the Boyer-Moore prover.[1] I wanted to show that the four axioms of arrays, which the simplifier assumed to be true, were valid in Boyer-Moore theory. Boyer and Moore had warned me of the soundness risks of adding axioms to their prover. So I tried to prove them from basic Boyer-Moore theory, which is close to the Peano axioms. Boyer-Moore theory is LISP-like in form. You start with (ZERO) and (ADD1 X). So two is represented as (ADD1 (ADD1 (ZERO))). It's all lists of tuples at the bottom. Equality is strict. (EQUAL A B) is true only if the representations of both A and B are identical. This creates a problem. An array can be represented as a list of (index, value), but for EQUAL to work, the list has to be ordered by subscript and each subscript unique. So storing into an array is represented as insertion into an ordered list. That generates a lot of special cases. Accessing an array is a linear list search by recursion: (DEFN selecta (A I) (IF (EQUAL (array-elt-subscript A) I) (array-elt-value A) (IF (EQUAL (array-prev A) (empty-array)) (UNDEFINED) (selecta (array-prev A) I)))) That's around line 3276 in [2]. The other definitions of array operations are similarly simple. Then we get to proving the classic four axioms of arrays. Around 3000 lines later, the classic four "axioms" of arrays have been proved. Much grinding through special cases. It's a neat result, but bulky. So I submitted a paper to JACM. Reviewer comments included "I hate to see something this complicated at the foundations of computer science", and just "This is unnecessary." People were really upset by all that case analysis. The theoretical problem was that I didn't have set theory. I could have built up set theory first, before array theory, then used set theory to prove array theory. That probably would have made mathematicians happier. Or not. Set theory is traditionally axiomatic, but it can be built up from constructive Boyer-Moore tuple theory if desired. I didn't argue with the reviewers. I probably could have found a more elegant path to this result, by creating intermediate lemmas, rather than letting the prover grind through the cases on automatic. But I wasn't going for a PhD. I had real work to do at an aerospace company. So, I've been beaten on by the academic community for a bulky machine proof. Today, nobody would be bothered by this approach. It's only a few thousand lines, and a human can follow it. You can be too early. (You can still run this prover today. I converted it to GNU Common LISP a decade ago. It takes about one second on a modern machine to go from the Peano-like axioms to array theory. It took 45 minutes on the VAX 11/780 I was using back in the early 1980s.) [1] https://github.com/John-Nagle/nqthm [2] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
logicallee
This post promotes child porn and ends with: "His advice? “Be of good cheer. You can continue in the same general line of research" and the statement that the slander and libel "is the tip of the iceberg, the thin end of the wedge and the first cuckoo of Spring". It's disgusting. I've flagged it.
Related Discussions
Found 5 related stories in 108.5ms across 9,386 title embeddings via pgvector HNSW
Discussion Highlights (8 comments)
evekayser
I think the same happens now with AI generating code. Nobody will read every line. that's part of the process from now on.
fhdkweig
The problem of the proof was that we knew that FCT was true, but we had no idea why. A good/elegant proof teaches us something new about how that problem is related to other problems. It isn't just about getting a true/false answer to the conjecture.
layer8
I didn’t know we had invented time machines yet. ;)
jjtheblunt
the title made me think of a much older machine that was used for calculating https://en.wikipedia.org/wiki/Antikythera_mechanism
jmount
I think a lot of great ideas like tree-width were developed in hope of simplifying the proof.
DonHopkins
>[...] mogged [...] Ixnay on the celinay ingolay.
Animats
That takes me back to an early 1980s incident where I was criticized for an early computer-generated proof. This was when I was building a program verifier at an aerospace company. We had the first SAT solver, the Oppen-Nelson simplifier, and the first constructive theorem prover, the Boyer-Moore prover.[1] I wanted to show that the four axioms of arrays, which the simplifier assumed to be true, were valid in Boyer-Moore theory. Boyer and Moore had warned me of the soundness risks of adding axioms to their prover. So I tried to prove them from basic Boyer-Moore theory, which is close to the Peano axioms. Boyer-Moore theory is LISP-like in form. You start with (ZERO) and (ADD1 X). So two is represented as (ADD1 (ADD1 (ZERO))). It's all lists of tuples at the bottom. Equality is strict. (EQUAL A B) is true only if the representations of both A and B are identical. This creates a problem. An array can be represented as a list of (index, value), but for EQUAL to work, the list has to be ordered by subscript and each subscript unique. So storing into an array is represented as insertion into an ordered list. That generates a lot of special cases. Accessing an array is a linear list search by recursion: (DEFN selecta (A I) (IF (EQUAL (array-elt-subscript A) I) (array-elt-value A) (IF (EQUAL (array-prev A) (empty-array)) (UNDEFINED) (selecta (array-prev A) I)))) That's around line 3276 in [2]. The other definitions of array operations are similarly simple. Then we get to proving the classic four axioms of arrays. Around 3000 lines later, the classic four "axioms" of arrays have been proved. Much grinding through special cases. It's a neat result, but bulky. So I submitted a paper to JACM. Reviewer comments included "I hate to see something this complicated at the foundations of computer science", and just "This is unnecessary." People were really upset by all that case analysis. The theoretical problem was that I didn't have set theory. I could have built up set theory first, before array theory, then used set theory to prove array theory. That probably would have made mathematicians happier. Or not. Set theory is traditionally axiomatic, but it can be built up from constructive Boyer-Moore tuple theory if desired. I didn't argue with the reviewers. I probably could have found a more elegant path to this result, by creating intermediate lemmas, rather than letting the prover grind through the cases on automatic. But I wasn't going for a PhD. I had real work to do at an aerospace company. So, I've been beaten on by the academic community for a bulky machine proof. Today, nobody would be bothered by this approach. It's only a few thousand lines, and a human can follow it. You can be too early. (You can still run this prover today. I converted it to GNU Common LISP a decade ago. It takes about one second on a modern machine to go from the Peano-like axioms to array theory. It took 45 minutes on the VAX 11/780 I was using back in the early 1980s.) [1] https://github.com/John-Nagle/nqthm [2] https://github.com/John-Nagle/pasv/blob/master/src/work/temp...
logicallee
This post promotes child porn and ends with: "His advice? “Be of good cheer. You can continue in the same general line of research" and the statement that the slander and libel "is the tip of the iceberg, the thin end of the wedge and the first cuckoo of Spring". It's disgusting. I've flagged it.