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.)
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.
Indeed, and the computer aided proof discouraged research into the insightful proof a lot of mathematicians think is probably out there to find. "Proved but not insightfully" is a problem status some mathematicians are starting to think of as closer to "open" than "closed", which is a good thing IMO. (I am not a mathematician, though)
> the computer aided proof discouraged research into the insightful proof a lot of mathematicians think is probably out there to find
Kempe's reduction technique, on which the eventual proof still depended (at least spiritually? I think?), did contain true insight with reach beyond the original problem statement (e.g., Chaitin/register allocation).
I submit that "clever way to soundly reduce to finite set and check" is itself probably one of the more important types of insight in mathematics. Actually, all of my favorite mathematics, from an aesthetic perspective, has exactly this flavor. That's down to taste, of course, but it is sort of a fundamental/powerful move in modern mathematics. The beauty of that insight can only be appreciated once you're willing to accept that boring case checking is tractable.
In that sense, the FCT gave us two really important insights -- first some profound insight from Kempe then an equally profound insight about the role of computers as a bicycle for human thought.
Maybe the new heuristic auto tactics will lower the cost of finding the human proof of the four color theorem enough to be affordable in the current environment.
I don't think it will be a problem for long, as AI systems evolve they will be able to find those elegant solutions and explanations for you in due time...
AI does not care for elegance. That's one of the problems with the bulk of AI generated code: even if it does the job it is between 3 and 5x as much code as you would normally use to do the same thing. And even if we conclude that this is fine as long as the tests pass it is a massive barrier to understanding. Good code is easy to read. AI generated code - the bulk of the AI generated code that I've been exposed to to date, to be more precise - is overly complicated. Elegance is to do that which needs doing, no more, no less.
I doubt that. I don't think AI are trained to find elegant solutions, they are trained to find solutions. if you look at the things that OpenAI published, so seem to be micro improvements riddled with chaos. They are better solution, but they aren't drastic.
I have noticed this with autoresearch too, the solutions and improvments that you get are incremental and not groundbreaking. Humans, have a way find elegant solutions and also seem to solve that problem. Then again, beauty is in the eye of the beholder, and I might be wrong.
Maybe the open problems are just by nature non-elegant and we human beings are bad at non-elegant mathmatics and found them either hard or not interesting before.
Mandelbrot comes to mind when thinking about the positive aspects of having a machine do some heavy lifting and showing patterns you wouldn't have noticed otherwise.
I'm not involved with proofs in math a lot but having a computer help with formalizing large parts of software so they end up more secure is a plus imo.
One of the most bizarre things from the past couple of years is how every single tech person that isnt living under a rock talks like a channer incel. It feels insane to me to see everyone say shit like "mogged", "-maxxing" or "-slop".
> I would like to conclude by telling a cautionary tale. Let us try and place the Antikythera Mechanism within the global context of ancient Greek thought. Firstly came the astronomers observing the motions of the heavenly bodies and collecting data. Secondly came the mathematicians inventing mathematical notation to describe the motions and fit the data. Thirdly came the technicians making mechanical models to simulate those mathematical constructions, like the Antikythera Mechanism. Fourthly came generations of students who learned their astronomy from these machines. Fifthly came scientists whose imagination had been so blinkered by generations of such learning that they actually believed that this was how the heavens worked. Sixthly came the authorities who insisted upon the received dogma. And so the human race was fooled into accepting the Ptolemaic system for a thousand years.
> Today we are in danger of making the same mistake over computers. Our present generation is able to view them with an appropriate skepticism when necessary. But our children's children may be brought up within a society dominated by computers, that they may actually believe this is how our brains work. We do not want the human race to be fooled again for another thousand years.
Applying this to today seems like a stretch. Short of some sort of mythical dark age style destruction of knowledge, what we have today benefits from widespread use of writing and other forms of communication which didn't exist back then.
It seems like the biggest risks come from willful ignorance of history, which we do see in some quarters but by no means all.
But people think it does, and it’s annoying. The past months I’ve often found mistakes and then heard the response along the lines of “oh Claude wrote that”.
It’s used as an excuse, and then the conversation just moves on. I don’t see a lot of accountability being taken. If anything, senior leadership sees it as a sign of adoption and accepts a certain level of risk.
You may have not understood at all what you have read.
Your quotation is attributed in the article to Bill Tutte, as his response to what shall do a mathematician when seeing computer-made mathematical proofs, “Be of good cheer. You can continue in the same general line of research" and that the first computer-made proof "is the tip of the iceberg, the thin end of the wedge and the first cuckoo of Spring".
For your information, in some European countries hearing a cuckoo was a traditional sign that the spring has come, in the ancient times when there were no meteorological prognoses, so like the other 2 comparisons it is appropriate for the first step of a progression.
I see nothing disgusting in this. It is just good advice that one should accept that computer-made proofs are here to stay and there will be more and more of them.
Did we read the same article? You’re quoting from the end, so it seems like you did at least skim the article. But this article has nothing to do with child porn? Where did you even get that idea? It’s talking about a famous mathematical proof.
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:
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...
thank you for sharing this story :) I’ve recently been enthralled with ACL2
I understand ACL2 now runs on SBCL.
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.
Indeed, and the computer aided proof discouraged research into the insightful proof a lot of mathematicians think is probably out there to find. "Proved but not insightfully" is a problem status some mathematicians are starting to think of as closer to "open" than "closed", which is a good thing IMO. (I am not a mathematician, though)
> the computer aided proof discouraged research into the insightful proof a lot of mathematicians think is probably out there to find
Kempe's reduction technique, on which the eventual proof still depended (at least spiritually? I think?), did contain true insight with reach beyond the original problem statement (e.g., Chaitin/register allocation).
I submit that "clever way to soundly reduce to finite set and check" is itself probably one of the more important types of insight in mathematics. Actually, all of my favorite mathematics, from an aesthetic perspective, has exactly this flavor. That's down to taste, of course, but it is sort of a fundamental/powerful move in modern mathematics. The beauty of that insight can only be appreciated once you're willing to accept that boring case checking is tractable.
In that sense, the FCT gave us two really important insights -- first some profound insight from Kempe then an equally profound insight about the role of computers as a bicycle for human thought.
1 reply →
Maybe the new heuristic auto tactics will lower the cost of finding the human proof of the four color theorem enough to be affordable in the current environment.
I don't think it will be a problem for long, as AI systems evolve they will be able to find those elegant solutions and explanations for you in due time...
AI does not care for elegance. That's one of the problems with the bulk of AI generated code: even if it does the job it is between 3 and 5x as much code as you would normally use to do the same thing. And even if we conclude that this is fine as long as the tests pass it is a massive barrier to understanding. Good code is easy to read. AI generated code - the bulk of the AI generated code that I've been exposed to to date, to be more precise - is overly complicated. Elegance is to do that which needs doing, no more, no less.
1 reply →
I doubt that. I don't think AI are trained to find elegant solutions, they are trained to find solutions. if you look at the things that OpenAI published, so seem to be micro improvements riddled with chaos. They are better solution, but they aren't drastic.
I have noticed this with autoresearch too, the solutions and improvments that you get are incremental and not groundbreaking. Humans, have a way find elegant solutions and also seem to solve that problem. Then again, beauty is in the eye of the beholder, and I might be wrong.
2 replies →
Maybe the open problems are just by nature non-elegant and we human beings are bad at non-elegant mathmatics and found them either hard or not interesting before.
It does though. To reduce from infinitely many graphs to a finite number of cases there is a lot of insight by itself.
Exactly.
> "The problem of the proof was that we knew that FCT was true"
Citation needed.
That was terrible phrasing. I meant "The problem with the proof was that although it showed that FCT was true, the proof did not explain why".
7 replies →
[dead]
I didn’t know we had invented time machines yet. ;)
We haven’t yet but we had then :-)
Mandelbrot comes to mind when thinking about the positive aspects of having a machine do some heavy lifting and showing patterns you wouldn't have noticed otherwise.
I'm not involved with proofs in math a lot but having a computer help with formalizing large parts of software so they end up more secure is a plus imo.
One of the most bizarre things from the past couple of years is how every single tech person that isnt living under a rock talks like a channer incel. It feels insane to me to see everyone say shit like "mogged", "-maxxing" or "-slop".
I still don't know what "mogged" means. "-maxxing" is ugly. "Slop" is the bon mot.
I think a lot of great ideas like tree-width were developed in hope of simplifying the proof.
the title made me think of a much older machine that was used for calculating
https://en.wikipedia.org/wiki/Antikythera_mechanism
> I would like to conclude by telling a cautionary tale. Let us try and place the Antikythera Mechanism within the global context of ancient Greek thought. Firstly came the astronomers observing the motions of the heavenly bodies and collecting data. Secondly came the mathematicians inventing mathematical notation to describe the motions and fit the data. Thirdly came the technicians making mechanical models to simulate those mathematical constructions, like the Antikythera Mechanism. Fourthly came generations of students who learned their astronomy from these machines. Fifthly came scientists whose imagination had been so blinkered by generations of such learning that they actually believed that this was how the heavens worked. Sixthly came the authorities who insisted upon the received dogma. And so the human race was fooled into accepting the Ptolemaic system for a thousand years.
> Today we are in danger of making the same mistake over computers. Our present generation is able to view them with an appropriate skepticism when necessary. But our children's children may be brought up within a society dominated by computers, that they may actually believe this is how our brains work. We do not want the human race to be fooled again for another thousand years.
-- E.C. Zeeman, Gears from the Greeks, January 1986, http://zakuski.utsa.edu/~gokhman/ecz/gears_from_the_greeks.p... (https://web.archive.org/web/20250502052226/http://zakuski.ut...)
Applying this to today seems like a stretch. Short of some sort of mythical dark age style destruction of knowledge, what we have today benefits from widespread use of writing and other forms of communication which didn't exist back then.
It seems like the biggest risks come from willful ignorance of history, which we do see in some quarters but by no means all.
1 reply →
I think the same happens now with AI generating code. Nobody will read every line. that's part of the process from now on.
The human who commits a bad change still takes the fall though. Automation doesn't absolve accountability.
But people think it does, and it’s annoying. The past months I’ve often found mistakes and then heard the response along the lines of “oh Claude wrote that”.
It’s used as an excuse, and then the conversation just moves on. I don’t see a lot of accountability being taken. If anything, senior leadership sees it as a sign of adoption and accepts a certain level of risk.
5 replies →
>[...] mogged [...]
Ixnay on the celinay ingolay.
There is now an opportunity for them to do it again by providing an easily understandable proof which isn't broken up into a large number of cases.
[flagged]
[dead]
[flagged]
You may have not understood at all what you have read.
Your quotation is attributed in the article to Bill Tutte, as his response to what shall do a mathematician when seeing computer-made mathematical proofs, “Be of good cheer. You can continue in the same general line of research" and that the first computer-made proof "is the tip of the iceberg, the thin end of the wedge and the first cuckoo of Spring".
For your information, in some European countries hearing a cuckoo was a traditional sign that the spring has come, in the ancient times when there were no meteorological prognoses, so like the other 2 comparisons it is appropriate for the first step of a progression.
I see nothing disgusting in this. It is just good advice that one should accept that computer-made proofs are here to stay and there will be more and more of them.
[flagged]
1 reply →
Did we read the same article? You’re quoting from the end, so it seems like you did at least skim the article. But this article has nothing to do with child porn? Where did you even get that idea? It’s talking about a famous mathematical proof.
What the actual fuck are you talking about??