Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Why doesn't mathematics collapse, though humans often make mistakes in proofs?

mathoverflow.net

Post reply on HN
Print view View original

61–70 of 85 posts

Re: Why doesn't mathematics collapse, though humans often make mistakes in proofs?

#61

Post by xvilka »

drchewbacca wrote: post #35
vbezhenar wrote: post #31

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.

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% complet…

Shouldn't it be written with Coq instead? Like UniMath[1] for example?

[1] https://github.com/UniMath

Re: Why doesn't mathematics collapse, though humans often make mistakes in proofs?

#62

Post by alanbernstein »

jokoon wrote: post #29

I 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…

Well, broadly speaking, pure mathematics is picking some axioms, and then proving rigorous results based on them. If that doesn't sound like a fun game to you, you don't need to play it or watch it.

Re: Why doesn't mathematics collapse, though humans often make mistakes in proofs?

#63

Post by parthpatel1001 »

matheist wrote: post #43
drchewbacca wrote: post #35

Earlier quoted context omitted.

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% complet…

> I am sure within 10 years every professional mathematician will use formal proofs. I'll take that bet. 1:1 odds, up to $50? Shall we say, every mathematician employed at an ivy league university math department (postdoc level or above) has published at least one paper which employs proof checking for at least some claim? (provided that they have published at all.) So I win if I can find at least one professor or po…

I just wanted to note how precise of a bet this is. I will be stealing the exact definition of conditions and contexts to which the bet applies, to future bets of my own.

Re: Why doesn't mathematics collapse, though humans often make mistakes in proofs?

#64

Post by dwohnitmok »

dwohnitmok wrote: post #52
pmoriarty wrote: post #49

Earlier quoted context omitted.

Although I am starting to get out of my depth, my impression was that ZFC itself is (per Godel's results) inconsistent or incomplete. Here is some research to this effect: If this is indeed the case (as it seems to my unprofessional first glance to be) then mathematics does not in fact have a solid foundation, despite its appeal to ZFC. I'd love to hear a professional logician weigh in on this, if there are any on he…

ZFC is incomplete. There are many celebrated results that are independent of ZFC (continuum hypothesis, large cardinals (a lot aren't even known to be consistent with ZFC), Suslin's Hypothesis, etc. However, by Godel we know this is true for any reasonable foundation of mathematics (i.e. anything capable of expressing the usual version of arithmetic). So it is not something that particularly troubles either logicians…

Oh I forgot to add. The inability to prove its own consistency is also something any reasonable foundation will have.

Re: Why doesn't mathematics collapse, though humans often make mistakes in proofs?

#65

Post by dwohnitmok »

dwohnitmok wrote: post #52
pmoriarty wrote: post #49

Earlier quoted context omitted.

Although I am starting to get out of my depth, my impression was that ZFC itself is (per Godel's results) inconsistent or incomplete. Here is some research to this effect: If this is indeed the case (as it seems to my unprofessional first glance to be) then mathematics does not in fact have a solid foundation, despite its appeal to ZFC. I'd love to hear a professional logician weigh in on this, if there are any on he…

ZFC is incomplete. There are many celebrated results that are independent of ZFC (continuum hypothesis, large cardinals (a lot aren't even known to be consistent with ZFC), Suslin's Hypothesis, etc. However, by Godel we know this is true for any reasonable foundation of mathematics (i.e. anything capable of expressing the usual version of arithmetic). So it is not something that particularly troubles either logicians…

Logicians are often unsatisfied with ZFC as a foundation for other reasons. These mainly amount to the clunkiness of set theory encodings. They have no notion of types so you can pose nonsense questions such as "is the number 2 a subset of the addition function?" There's no formal way of dealing with objects "larger" than sets (e.g. the collection of all sets) other than as syntactic formulas. They obscure relationships between different mathematical fields by resulting in completely different encodings for analogous structures.

This is why logicians will sometimes talk your ear off about how category theory is so much better as a foundational theory than set theory.

Again though, for the working mathematician, these flaws in ZFC as a foundation rarely matter.

Re: Why doesn't mathematics collapse, though humans often make mistakes in proofs?

#66

Post by guerrilla »

galaxyLogic wrote: post #36

Think 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 c…

The vast majority of mathematics is classical, not intuitionistic, just so you know.

Re: Why doesn't mathematics collapse, though humans often make mistakes in proofs?

#67

Post by alexmlamb »

galaxyLogic wrote: post #38
brianberns wrote: post #14

Earlier quoted context omitted.

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…

I don't think it's necessarily like that. The error could make the theorem wrong in all cases.

I think it's more that the mathematician has a top-down way of reasoning, where they can see things like "I want to get from New York City to Los Angeles, so I have to board the bus, take a flight, and then take the bus from the airport at LA". There are certain parts where you basically know that a proof will be possible, because it seems true, like "I can get to LA's airport with public transit", so usually a specific hiccup, like a bus being delayed, won't prevent you from getting there.

Re: Why doesn't mathematics collapse, though humans often make mistakes in proofs?

#68

Post by harry8 »

There is no proof in science and we observe it doesn't suffer from wholesale collapse.

Things being proved in mathematics are unlikely to be wildly wrong even without proof. Fermat's theorem being an example of one that took a very long time to be proved and basically nothing changed when it was. We were already convinced it was true by brute force failure to find a counter example. This lack of proof but search for counter-example is basically the scientific method. Is A equivalent to B? Prove it? Or write a for-loop and test it for values you care about. If you think you've proved it you probably write the for loop anyway (where such a thing is feasible).

So do we actually /need/ proof in math at all or is it just good fun and properly satisfying for mathematicians? Perhaps these are two extremes and case-by-case we could plot them somehwere between the two. Some right up hard against one side or the other.

So is P=NP? There is no proof. You probably aren't going out on a massive limb to have a view on the matter without it.

Re: Why doesn't mathematics collapse, though humans often make mistakes in proofs?

#69

Post by new2628 »

triska wrote: post #28
hyperpape wrote: post #27

Earlier quoted context omitted.

Mochizuki’s paper seems like a debatable example. Many mathematicians have been baffled by the proof or ended up feeling that it was not that promising, even prior to attempting to do a detailed analysis. If it’s unrecoverable, then the community will look good for its hesitation. https://news.ycombinator.com/item?id=15971802

Take for instance Wu-Yi Hsiang's suggested proof of the Kepler conjecture as a less controversial example. Quoting from https://en.wikipedia.org/wiki/Kepler_conjecture : "The proof was praised by Encyclopædia Britannica and Science and Hsiang was also honored at joint meetings of AMS-MAA." Which is followed, after a few sentences, by: "The current consensus is that Hsiang's proof is incomplete."

Or Kempe's (mistaken) proof of the 4 color theorem.

Re: Why doesn't mathematics collapse, though humans often make mistakes in proofs?

#70

Post by moomin »

dwohnitmok wrote: post #48
pmoriarty wrote: post #22

Earlier quoted context omitted.

My memory from the logic classes I've taken was that after Godel, mathematicians largely abandoned Hilbert's, Russell's and Whitehead's ambition of founding mathematics on logic, and largely grew disinterested in foundational issues as a whole. As such, mathematics doesn't have a solid foundation, and most contemporary mathematicians seem to be ok with that, as long as it works and they can get interesting results.

I agree with the rest of what you wrote, but doesn't have a solid foundation seems a bit far. Mathematicians hand-wave that their proofs can be reduced to ZFC set theory and despite reasonable wariness about that hand-waving, it has so far been borne out by all efforts at deeper inspection all the way up to full machine-checked formalization.

TBH, the construction of Riemann surfaces from the natural numbers is pretty well understood by the average UK undergraduate. (Natural->Integer->Rational->Real->Complex->Foundations of Reimann Surfaces). The expression of the rules of natural numbers in ZFC is fully understood by far fewer, but that’s mostly because it’s tedious.
Post reply on HN