Number Theorist Fears All Published Math Is Wrong

[FBInCIAnNSATerroristSlayer]

https://www.vice.com/en_us/article/8xwm54/number-theorist-fears-all-published-math-is-wrong-actually?utm_campaign=sharebutton


Number Theorist Fears All Published Math Is Wrong



"I think there is a non-zero chance that some of our great castles are
built on sand," he said, arguing that we must begin to rely on AI to
verify proofs.


by Mordechai Rorvig

Sep 26 2019, 12:30pm

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.