It is probably obvious that whether a proposition is (necessarily) true is different than proving, in some formal system, that it is true. It is also clear that if you don’t have a formal proof for a true proposition, your lack does not make the proposition false.
It is less obvious that, sometimes, adequate proof of a truth of a proposition is intuition (see this award-eligible internationally selling book for why). Sometimes we can “see” or “feel” a proposition is true, though we have no way of knowing how to prove it true in a formal system, such as a mathematical system. Though, often enough, diligent effort will reveal how the proposition can be shown true in such a system, or even in more than one system. There exist multiple proofs for many mathematical theorems.
Intuition can mislead. The inner sight we have can blur. Scrooge’s underdone potato can cause one to see ghosts. This puts intuition in a bad light, to the unfortunate extent it is never trusted in some circles. Well, a car sometimes breaks down and crashes, but this is not poof that cars never reach their destination.
On the other side, so-called rigorous proofs can lead one to a false destination, too, particularly if the road is long and arduous. Just one tiny invisible error can render an entire of chain of reasoning faulty. One false premise is all it takes.
It’s worse when a suspect chain stretches out over decades, argument building upon argument, each segment built by different people. No chance of going through the whole thing yourself. Also consider the strangest errors can creep in by refusing to look at the anchors, which may be corroded and pitted, or made of foam and not steel, rendering whole areas a mess.
The problem is not new.
This fellow Kevin Buzzard, “a number theorist and professor of pure mathematics at Imperial College London”, is worried.
New proofs by professional mathematicians tend to rely on a whole host of prior results that have already been published and understood. But Buzzard says there are many cases where the prior proofs used to build new proofs are clearly not understood. For example, there are notable papers that openly cite unpublished work. This worries Buzzard.
“I’m suddenly concerned that all of published math is wrong because mathematicians are not checking the details, and I’ve seen them wrong before,” Buzzard told Motherboard while he was attending the 10th Interactive Theorem Proving conference in Portland, Oregon, where he gave the opening talk.
“I think there is a non-zero chance that some of our great castles are built on sand,” Buzzard wrote in a slide presentation. “But I think it’s small.”
Buzzard thinks he has a solution: computerized proofs, a.k.a. “proof verification software”.
This could work to some small extent, for example in finding “typos” in theorems. Few object to this kind of software. But the comes the hype and exaggeration typical in computer science:
Ultimately, computer scientists would like to create a general automated theorem prover, a software system that can create its own proofs, do its own math.
Won’t happen. Not in any interesting sense. Computers cannot see; they do not have intuitions. They therefore do not and will never know when new direction is worth exploring. No great idea comes from the logical concrete mechanical side of proofs, which computers can aid. All truly beautiful ideas come from minds which can grasp the infinite.
Infinite?
There are an infinity of necessarily true propositions. For example, “2 > 1”, “3 > 2”, “4 > 3”, and so on. Almost all are boring like these. Many are even more boring. Once can’t say “useless”, because what is true cannot be without use. But no one would think these propositions worth contemplation. It requires a mind, like we have, to contemplate. Computers don’t think; they are only mindless adding machines.
That means if you set them off calculating under a given set of rules, they will indeed find true propositions consistent with those rules. But since most propositions are of little or no real interest, computers will instead create a lot of busy work for those who have to sort through the output.
It will in particular cause people to overrate banalities because they are “computer” or “AI approved”.
To support this site and its wholly independent host using credit card or PayPal (in any amount) click here
Wasn’t the 4-colour map theorem proved using a computer? To slog through manual calculations that were otherwise impractical?
How can you program a computer to do Math that hasn’t been programmed into it?
There is a tremendous faith in computers that is completely wrong and dangerous. Input/output is 100% dependent on the programmer and the program. I was reading a post on one of those nefarious right-wing sites where the writer was asking on Twitter WHY did Walgreens have a SOGI screen with only a few options? Why not an open-ended question—write what you believe you are. The conversation included things like:
“On the contrary – I’m simply pointing out the futility of creating a finite list of genders for purposes of this sort of questionnaire. It’s caving to nonsense, and it creates more problems than simply asking an open ended question.” (Writer)
“Those arguing for this nonsense have obviously never built a database or managed its contents. I disagree w/ the open-ended option because the data would be unmanageable, …” (programmer)
Writer points out that “names” in a field are open-ended and yet somehow the database manages those. This was met with much anger and insulting.
“I guarantee you that people who use traditional pronouns are too ignorant to know how to answer. Even if you could make that field dynamic, most Americans are not smart enough to know what a pronoun is. I’m serious.” (programmer, changing the subject because he cannot answer the statement about why no open-ended questions.)
The tweet thread continued with the programmers making up more and more excuses for why programming cannot handle an open answer in one field but breezes right through for another. In the end, the answer was the programmer wants you to answer a certain way because they BELIEVED that was the RIGHT way (in this case, based on denial of reality and science). This is going to infect every single program out there—a programmer puts in their own beliefs and excludes those they do not like. Even in mathematics. Intuitive leaps simply cannot occur because said things are deliberately removed from possible outcomes. Confirmation bias, etc are all human traits that become part of the “not-so-pure” computer code. Computers are their programmers, not AI’s.
@Sheri — I have been that programmer. Except arguing from the other side. Why should I create a select list of addresses for every address in the country when someone can just type it in, validate the address against a known list and keep moving forward. Why is it that I have to type City, State and Zip, when I should be able to just put in the zip and the rest gets looked up? Some people don’t know their own zip.
This might be seen as the multiple choice problem. Multiple choice tests are usually easier because 4 answers can usually be whittled down to 2 by removing the obviously false answers. What is a select list, but a really fancy multiple choice answer?
I like to think of 2 lego bricks 1×2 and ask “How many ways can these 2 bricks be put together?” Then ask it from the perspective of a programmer.. How many fields do I need to represent those ways. 1 field can easily represent it, but we will infuse that one field with many, many, many options by making it open. If I try and contain the possible forms of entry, the number of fields starts to increase.
The number of ways those 2 1×2 blocks can be connected is somewhere between 2 and a sideways 8. For me, this is the proof that computers shouldn’t try and make proofs. Contained in that single field is infinity. I asked a mathematician on Quora “What is the graham’th digit of pi?” It was meant to be an irrational question pointing at the same problem. Numberphile suggests that if you were able to conceive of all of the digits of graham’s number, your brain would become a black hole.
All of this is me attempting to agree with you.
I thought Turing pretty much proved the insanity of this proposition?
I thought that Godel’s Theorem guarantees that in principle, a computer will never discover a truly new theorem–at best, it will produce novel combinations of known theorems. Computers have no intuition. Humans do.
Jerry,
Godel’s Theorem is about the incompleteness of formal systems and the existence of unprovable statements within those systems. It really has nothing to do with discovery of new theorems.
Intuition is the ability to acquire knowledge without recourse to conscious reasoning. Which means without being aware of the how. Why is this important?
I wonder if Professor Buzzard believes that an AI could prove any of the Millenial Prize Problems? And what would the AI do with the prize money?
I’ve been intrigued by one of the MPPs, the Riemann Hypothesis, mainly because some of the plots associated with the Zeta function look strikingly similar to plots associated with IIR (infinite impulse response) delay line filters. The math is way, way, way over my head, but . . . if the Zeta function could be recast as an IIR delay line filter (or, more likely, as an infinite number of such filters), then maybe an engineering shortcut could be brought to bear on the problem.
But, would the mathematics world accept an engineering shortcut as a proof? For example, conservation of energy? An IIR delay line filter is a real thing that can be built, therefore conservation of energy must apply.
Professor Briggs, I notice that you often mention your Uncertainty book. I’m pretty careful about what I spend my money on these days; the last thing I want to do is harm the planet. Is your book Dolphin-Free?
A friend of mine, who is a very good mathematician with a number of published papers, worked in the area of “Automated Theorem Proving” for a number of years. They managed to verify some certainly nontrivial results with the system they worked on. I don’t remember whether any new, significant results were found.
He mentioned to me that the system they were using is now somewhat in limbo because the developers are no longer actively working on it. (I think it was a Prolog listener of some sort.) What seems to me to be a very material consideration is that they were working in an area of abstract algebra (module theory), where everything is naturally symbolic to begin with. If one works in certain areas of topology, though, I’d really have to wonder how one can truly translate the objects one is studying into a finite list of symbols. There is “combinatorial topology,” of course, and geometric group theory, which are amenable to computational treatment at least to some extent. But I highly doubt whether certain other areas of geometry or topology could really be handled well being limited to computational means.
So, a computer cannot intuit because it is not a living being. Computers cannot receive inspiration by the Holy Spirit. It has no created, by God, life.
Computers are programmable machines, subject to the information given to them, with which they can compute to a certain degree, but which workings with the inputed information, have a set limit, and when that limit is reached, the computers can go no further without added or subtracted information.
God bless, C-Marie