A number theorist and professor of pure mathematics, Kevin Buzzard, at Imperial College London, believes that it is time to create a new area of mathematics devoted to the computerization of proofs.
If you are starting to feel a sense of dread well up inside you, yes, we are talking about those proofs we all had to struggle through in high school.
And if you have shoved those memories deep enough to where you forget what a proof actually is — it is a demonstration of the truth of a mathematical statement. The purpose of having such things is, in theory, by proving things while learning new techniques of proof — people gain an understanding of math.
Currently, the greatest proofs have become so complex that almost no human on earth can understand all of their details — let alone verify them. Buzzard is afraid that many of these proofs that have been believed to be true all this time — are actually incorrect.
You are asking for an example? You got it.
Get the gist? Great.
Now, new proofs by professional mathematics tend to heavily rely on a lot of prior results that have already been accepted, published and understood.
That being said, Buzzard says there are many times where the prior proofs to build new proofs are not concisely understood. For example, there are notable papers that openly cite unpublished work. Buzzard explains how this is an issue.
“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 revealed to Motherboard while he was attending the 10th Interactive Theorem Proving conference.
“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.”
When it comes to new mathematics, there are checks and balances — every step must be verified. But there are senior experts and elders of the mathematical community who give a reliable testimonial guide to what is true or not (as the thinking goes) and if an elder cites a paper and uses it in their work — then that paper most likely does not need to be checked.
Buzzard brings attention to this by stating how modern mathematics has become overdependent on the word of elders as results continue to grow more complex. A brand new proof may cite 20 other papers while just one of those 20 may involve 1,000 pages of reasoning.
That being said, if a respected senior mathematician cites the 1,000 page paper, many other mathematicians may just assume the 1,0000-page paper (as well as the new proof) is true and won’t double check it.
But mathematics is designed to be universally provable and therein lies the issue at hand.
The over reliance on the elders leads to a murky understanding of what is true and what is not.
Proposed in 1637, a proof of Fermat’s Last Theorem was once considered by the Guinness Book of World Records to be the world’s “most difficult math problem,” later published in the 1990s.
Buzzard claims that no one actually understands it or knows if it is true.
Buzzard saw talks by senior mathematicians, Thomas Hales and Vladimir Voevodsky, a few years back that introduced him to proof verification software that was become very good. With the software, proofs can be systematically verified by computer — taking the responsibility out of hearsay by elders.
When Buzzard began using the proof verification software called Lean, he became instantly addicted.
To verify their proof — a Lean user has to formalize the proof or convert it from human language and symbols into the programming language of Lean. The user in addition also must formalize any subsidiary definitions as well as proofs that their new work relies on.
If these challenges can be achieved, Buzzard believes this software can make leaps and bounds beyond just proofs in the math world: as in a software system that can do its own math.
If you ask me, that adds up.