Interesting set of slides. http://wwwf.imperial.ac.uk/~buzzard/one_off_lectures/msr.pdf I've advocated a similar project for years -- somewhat akin to Wikipedia, except that a "Wikimath" won't accept entries that its proof checker can't verify. Unlike Wikipedia, which is susceptible to human bias & error, such a Wikimath could be more reliable and neutral. But if you believe in all the progress in AI/ML/QC, computers will be able to understand our non-formalized proofs, so why is all this necessary? ;-) ;-) ;-) ;-) At 10:33 PM 9/27/2019, Ray Tayek wrote:
https://science.slashdot.org/story/19/09/26/223218/number-theorist-fears-all...
Posted by BeauHD <https://twitter.com/BeauHD> on Thursday September 26, 2019 @11:30PM from the future-of-mathematics dept.
An anonymous reader quotes a report from Motherboard:
/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 <https://www.vice.com/en_us/article/8xwm54/number-theorist-fears-all-published-math-is-wrong-actually>.
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 <https://itp19.cecs.pdx.edu/> 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 <http://wwwf.imperial.ac.uk/~buzzard/one_off_lectures/msr.pdf>.
"But I think it's small."
-- Honesty is a very expensive gift. So, don't expect it from cheap people - Warren Buffett http://tayek.com/