I think that mathematicians should strive to use formal language proofs verified by computer. It'll allow to avoid situations when it's unclear whether this proof is correct or not and it'll allow people not to waste time on checking whether that proof is correct.
Why doesn't mathematics collapse, though humans often make mistakes in proofs?
31–40 of 85 posts
Re: Why doesn't mathematics collapse, though humans often make mistakes in proofs?
#32because "maths" will always be the consensus. you cant break it, only make it not work. >:3
Re: Why doesn't mathematics collapse, though humans often make mistakes in proofs?
#33Collapses are rare indeed, but they do happen. Cf . the collapse of the Italian School of Algebraic Geometry [1], the cleanup of which took all the efforts of Grothendieck et al . [1] https://en.wikipedia.org/wiki/Italian_school_of_algebraic_ge...
That's pretty incredible, thanks for sharing. Hard to believe decades of mathematical research collapsed on itself.
Re: Why doesn't mathematics collapse, though humans often make mistakes in proofs?
#34Ted Chiang’s short story “Division by Zero”, about a mathematician who discovers the foundations of mathematics are inconsistent, would appear to be relevant to this discussion.
Re: Why doesn't mathematics collapse, though humans often make mistakes in proofs?
#35I think that mathematicians should strive to use formal language proofs verified by computer. It'll allow to avoid situations when it's unclear whether this proof is correct or not and it'll allow people not to waste time on checking whether that proof is correct.
I have done a little with http://us.metamath.org/ and I am sure within 10 years every professional mathematician will use formal proofs.
The two prerequisites are 1) making a fluid and intuitive interface for inputting proofs which can also display human readable proofs for any theorem known and 2) creating a database of all known mathematical proofs into which new results can be inserted.
Both tasks are ~50% complete. Metamath, for example, has all of mathematics formalised up to a basic undergraduate level. It has some reasonable editing software, but not close to good enough for mass adoption. There are also plenty of other systems being developed.
The time will come though relatively soon.
Re: Why doesn't mathematics collapse, though humans often make mistakes in proofs?
#36Think about Curry Howard isomorphism which says programs are proofs and data-types are theorems.
A lemma is then like sub-routine.
If there is something wrong in the sub-routine it can often be fixed without requiring any changes to the callers of the sub-routine. It might be the case that the subroutine can never produce a value needed by its callers without changing the types of arguments fed to it, and in such a case it is not enough to fix the subroutine.
But in many cases just the lemma-subroutine needs to be corrected, and the rest of the program, rest of the proof can be used as is.
https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...
Re: Why doesn't mathematics collapse, though humans often make mistakes in proofs?
#37I have never understood why proofs are always required. Usually when you have an unproven theorem and it works often enough, to me it's good enough for most of what you're doing, for example in applied math. Of course if you find places where an unproven theorem doesn't work, it becomes interesting to why it doesn't work, and it's usually a big discovery, but it doesn't really disprove a theorem, it just helps to ref…
If some claim is not proved but believed to be true it's called a conjecture. If a claim is known to be false but "works often enough" it's called a heuristic.
Re: Why doesn't mathematics collapse, though humans often make mistakes in proofs?
#38If builders of a huge castle place some stones incorrectly, does it collapse completely? No. Such errors may be discovered soon and taken down, or stand for decades, sometimes with lots of stuff built on top of it, and sometime parts will collapse, but the overall structure of the castle is sound, and, sooner or later, errors will be corrected. And of course, sometimes, somebody decides to start building an entire ne…
The analogy I’d make is to bugs in software. Most software has bugs, but they’re only triggered in specific circumstances. Stay away from those cases and you’re usually fine. If you happen to hit a new bug, you might lose some data, but it’s not going to render the entire application useless.
So a proof might claim to prove a theorem about a whole class of numbers or other mathematical objects. But if there is bug in one of its lemmas it would mean its results are true of only a subset of the mathematical objects claimed. That would be like getting an error on specific inputs.
The proof then remains a valid proof of something although not exactly a proof of everything its authors claim it to be a proof of.
An erroneous proof is also usually useful because it is not clearly wrong in most cases since nobody has come up with counter-examples so far that would prove the proof incorrect, yet.
Re: Why doesn't mathematics collapse, though humans often make mistakes in proofs?
#39Ted Chiang’s short story “Division by Zero”, about a mathematician who discovers the foundations of mathematics are inconsistent, would appear to be relevant to this discussion.
Could you share more or summarize?
Re: Why doesn't mathematics collapse, though humans often make mistakes in proofs?
#40Mathematical physics and engineering holds up to empirical scrutiny.
Exactly this. Mathematics provides an imperfect model that needs to be adjusted for engineering problems in the messy, real world.
Maybe true about physics (as physics does strive to provide approximate models of reality), but mathematics is abstract and for most mathematicians any application to reality is coincidental. You might enjoy reading "The unreasonable effectiveness of mathematics" (it is many decades old, but recently a lot of CS essays copy the style and title).