Number theorist fears many proofs widely considered to be true are wrong
1–10 of 107 posts
Re: Number theorist fears many proofs widely considered to be true are wrong
#2Vice really does a disservice to the author. "All" math is not wrong, but I sure wish theorem provers were the preferred method of formalizing mathematics. But theorem provers really aren't quite ready for prime time either. But it sure feels like a lot of verification of mathematics is somewhat repetitive.
I think that programming/CS is to mathematics what neolithic revolution was to human culture. It allows for specialization in the stack. People can obsessively optimize different parts of the stack to everyones benefit.
Re: Number theorist fears many proofs widely considered to be true are wrong
#3Headline is of course absurd hyperbole that does not belong here.
> "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."
Re: Number theorist fears many proofs widely considered to be true are wrong
#4Soo... Unit testing / CI for math proofs? If it can be done in software, great.
Re: Number theorist fears many proofs widely considered to be true are wrong
#5There is a big grey area between "not 100% correct" and "wrong and harmful". Like a faulty computer program that produces correct results in 99.999% of the cases a wrong mathematical statement can still yield useful results in practice. You just don't want to run into those pesky edge cases where it indeed is wrong.
Having a database of all mathematical proofs where all of them are checked for validity, however, is a very useful tool to actually find those edge cases where a proof is wrong and give future mathematicians a solid foundation.
Using AI as an extension of human capabilities is a given to me. Like with heavy machinery, we don't want to do the heavy lifting. We want to steer it properly to gain most benefit.
Re: Number theorist fears many proofs widely considered to be true are wrong
#6Headline is of course absurd hyperbole that does not belong here. > "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."
Yes, the title ought to be changed. At least, "all" to "some".
But he does note:
> 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.
Re: Number theorist fears many proofs widely considered to be true are wrong
#7Soo... Unit testing / CI for math proofs? If it can be done in software, great.
To my knowledge the hard part is writing the input for the software. While in text you have a bit of leeway to glance over some details, with the computer program you must, indeed, write every last relevant detail down and you must get it right. This is very heavy work.
Re: Number theorist fears many proofs widely considered to be true are wrong
#8Sounds like a sales pitch for Lean (Microsoft's theorem prover), even though Coq [1] is the standard tool for the UniMath [2] project.
Re: Number theorist fears many proofs widely considered to be true are wrong
#9Headline is waaaay overblown, but not all of it is total hyperbole -- checkout out arxiv and try to read the abstract from just about any paper.
It's basically totally impermeable. I'm almost done with an undergraduate degree in math and basically have no idea what ~90% of the research is about at anything other than a topical level. This is fine, it's written for specialists in the field (hopefully), but damn, for most fields, it's not a whole lot of people.
Compared to physics or chemistry, math gets very specialized, very quickly. Depending on the field, there's no easy real world isomorphisms either, making it even more difficult.
Re: Number theorist fears many proofs widely considered to be true are wrong
#10Soo... Unit testing / CI for math proofs? If it can be done in software, great.
To my knowledge the hard part is writing the input for the software. While in text you have a bit of leeway to glance over some details, with the computer program you must, indeed, write every last relevant detail down and you must get it right. This is very heavy work.
But it's once-off work. Thereafter the computers can take over.