On Monday, September 30, 2019 at 2:37:36 AM UTC+3, FBInCIAnNSATerroristSlayer wrote:
> 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.