Sep 28, 2019 09:28 PM
https://www.vice.com/en_us/article/8xwm5...g-actually
EXCERPT: . . . "I think there is a non-zero chance that some of our great castles are built on sand," Kevin 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.” (MORE - details)
EXCERPT: . . . "I think there is a non-zero chance that some of our great castles are built on sand," Kevin 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.” (MORE - details)