There is an infection of software in pure mathematics. Some of the heavyweight intellects of the field, renowned for their self-reliance, are starting to turn to software to help them understand and verify proofs.
Kevin Buzzard, a number theorist and professor of pure mathematics at Imperial College London, believes that it is time to create a new area of mathematics dedicated to the computerization of proofs. The greatest proofs have become so complex that practically no human on earth can understand all of their details, let alone verify them. He fears that many proofs widely considered to be true are wrong. Help is needed.
What is a proof? A proof is a demonstration of the truth of a mathematical statement. By proving things and learning new techniques of proof, people gain an understanding of math, which then filters out into other fields.
To create a proof, begin with some definitions. For example, define a set of numbers such as the integers, all the whole numbers from minus infinity to positive infinity. Write this set as: ... , -2, -1, 0, 1, 2, ... Next, state a theorem, for example, that there is no largest integer. The proof then consists in the logical reasoning that shows the theorem to be true or false, in this case, true. The logical steps in the proof rely on other, prior truths, which have already been accepted and proven. For example, that the number 1 is less than 2.
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."
New mathematics is supposed to be proven from the ground up. Every step must be checked, or at least the reasoning followed. On the other hand, there are senior experts and elders of the mathematical community who provide a reliable testimonial guide to what is true or not true. If an elder cites a paper and uses it in their work, then the paper probably doesn’t need to be checked, the thinking goes.
Buzzard’s point is that modern mathematics has become overdependent on the word of the elders because results have become so complex. A new proof might cite 20 other papers, and just one of those 20 might involve 1,000 pages of dense reasoning. If a respected senior mathematician cites the 1,000 page paper, or otherwise builds off it, then many other mathematicians might just assume that the 1,000-page paper (and the new proof) is true and won't go through the trouble of checking it. But mathematics is supposed to be universally provable, not contingent on a handful of experts.
This overreliance on the elders leads to a brittleness in the understanding of truth. A proof of Fermat's Last Theorem, proposed in 1637 and once considered by the Guinness Book of World Records to be the world's "most difficult math problem," was published in the 1990s. Buzzard posits that no one actually completely understands it, or knows whether it's true.
"I believe that no human, alive or dead, knows all the details of the proof of Fermat’s Last Theorem. But the community accept the proof nonetheless," Buzzard wrote in a slide presentation. Because "the elders have decreed that the proof is OK."
A couple of years ago, Buzzard saw talks by the senior mathematicians Thomas Hales and Vladimir Voevodsky that introduced him to proof verification software that was becoming quite good. With this software, proofs can be systematically verified by computer, taking it out of the hands of the elders and democratizing the status of truth.
When Buzzard started using the proof verification software called Lean, he became hooked. Not only did the software allow him to verify proofs beyond any doubt, the software also promoted thinking about math in a clear and unmistakable way.
“I realized the computers would only accept inputs in a very precise form, which is my favorite way of thinking about math,” Buzzard said. “I fell in love, because I felt like I found a soulmate. I found something that thought about math just the way I thought about it.”
To verify their proof, a user of Lean has to formalize the proof, or convert it from human language and symbols into the programming language of Lean. The user must also formalize any subsidiary definitions and proofs that their new work relies on. Though this conversion process is labor-intensive, Lean seems to be able to handle any math that Buzzard throws at it, distinguishing it from other proof assistant programs.
Lean has drawn interest from a growing community of mathematicians, particularly in teaching. Jeremy Avigad is a Professor at Carnegie Mellon who specializes in proof theory. Both Avigad and Buzzard have started using Lean in introductory college classes on proof. The software checks the veracity of each line of a proof and reports feedback, which is helpful for students.
Though Avigad is excited about the community that has taken an interest in Lean, he cautions that the technology still needs improvement. Proof assistants are time-consuming to use. “The field has been around for a few decades and things are getting better, but we’re not there yet,” he said.
If these challenges can be overcome, Buzzard thinks that the software can have even broader effects beyond proof. Take for example the problem of search. Huge amounts of new results are published every year, at a breakneck pace, making searching through these proofs extremely important.
Hales and Buzzard have pointed out that if all new paper abstracts were entered in Lean, then any mathematician could query the database of these abstracts for a precise Lean mathematical object and find out all that was known about it. To some extent, the inscrutable brains of the elders could be turned inside out.
Computer scientists could use such a database as a training ground for AI’s. Because the results in such a database would be defined in the precise language of Lean, they would be much easier for a program to learn from compared with results written in idiosyncratic English.
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. Automated provers rely on the same technology as Lean to determine whether a proof is true. The increasing adoption of Lean may turn out to be an important formative step towards the overall automation of math.
The Helix Center on the upper east side of Manhattan will host a roundtable discussion of the automation of math on October 5, live streamed from YouTube and its website. Michael Harris, professor of mathematics at Columbia University and a colleague of Buzzard’s, will participate in the forum.
Harris is concerned that the computer scientists and tech companies who want to automate math don’t share the same motivations as mathematicians. Computer scientists, for example, want to use the technology behind Lean to verify that programs are bug-free. Companies want to make profit. Mathematicians like Buzzard just want to do math.
“One thing I can predict is if really smart people like Thomas Hales and Buzzard continue to think along these lines, then something interesting is going to come out of it; it may not be AI but it may be whole new branches of mathematics or whole new ways of thinking," Harris said.
from VICE https://ift.tt/2ljwAl7
via cheap web hosting
No comments:
Post a Comment