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.
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