Why doesn't mathematics collapse, though humans often make mistakes in proofs? • Hacker News Board

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

#81

Post by liuyao » Tue, Aug 20, 2019, 2:52 AM UTC

gone35 wrote: post #24

Collapses 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...

Great example. Weil is said to be the one who was deeply immersed in both the geometric tradition of the Italians and the functional perspective of Riemann, so he was in a unique position to see many analogies and deep connections. (He proved small pieces of it, and laid the roadmap for Grothendieck.) These are the kind of “ideas and understanding” that Schulman is talking about.

What collapsed were the proofs, and some if not all of the ideas survived and got painted over with the new language. Sadly algebraic geometry has this bad reputation of being obtuse and opaque, that it has become devoid of geometry. Mathematics need to be more open about ideas that are not rigorous, not just left unspoken between the experts themselves.

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

#82

Post by fnrslvr » Tue, Aug 20, 2019, 8:41 AM UTC

heyitsguay wrote: post #56

dwohnitmok wrote: post #46

Earlier quoted context omitted.

AFAICT mathematical logic has always felt like a curious side show in the greater math community. If you were to ask professional mathematicians to list off all the axioms of ZFC they'd probably shrug if they didn't get all of them. They probably wouldn't know about the more exotic parts of set theory such as large cardinals nor would they would probably know too much about alternate foundations of mathematics. They…

That's because formal logic is a (relatively) recent attempt to formalize the intuitions behind the math that people were already doing. Doing mathematics doesn't really depend on foundational logic in the same way that, e.g., a web app depends on transistor physics. As somebody once said, if we ever found a contradiction in the ZFC axioms, we wouldn't throw out math, we'd just throw out ZFC.

> Doing mathematics doesn't really depend on foundational logic in the same way that, e.g., a web app depends on transistor physics.

Web apps don't depend on transistor physics at all, though. An important consequence of Turing universality is that computer science is not a subfield of electrical engineering.

Also, mathematics underwent very dramatic transformations during the late 1800s and early 1900s alongside the early development of formal logic and set theory. To say that logicians were merely "formalizing the intuitions behind the math that people were already doing" strikes me as misguided at best. The mathematics that rose to prominence in that era was very different from what preceded it, often controversially so.

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

#83

Post by dorgo » Tue, Aug 20, 2019, 8:58 AM UTC

heyitsguay wrote: post #56

dwohnitmok wrote: post #46

Earlier quoted context omitted.

AFAICT mathematical logic has always felt like a curious side show in the greater math community. If you were to ask professional mathematicians to list off all the axioms of ZFC they'd probably shrug if they didn't get all of them. They probably wouldn't know about the more exotic parts of set theory such as large cardinals nor would they would probably know too much about alternate foundations of mathematics. They…

That's because formal logic is a (relatively) recent attempt to formalize the intuitions behind the math that people were already doing. Doing mathematics doesn't really depend on foundational logic in the same way that, e.g., a web app depends on transistor physics. As somebody once said, if we ever found a contradiction in the ZFC axioms, we wouldn't throw out math, we'd just throw out ZFC.

>if we ever found a contradiction in the ZFC axioms, we wouldn't throw out math, we'd just throw out ZFC.

It's like saying: if we ever found a contradiction in the base case of a mathematical induction, we wouldn't throw out mathematical induction, we'd just throw out the base case. The indudction step remains sound.

https://en.wikipedia.org/wiki/Mathematical_induction

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

#84

Post by drchewbacca » Tue, Aug 20, 2019, 12:54 PM UTC

xvilka wrote: post #61

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…

Shouldn't it be written with Coq instead? Like UniMath[1] for example? [1] https://github.com/UniMath

There are quite a few competing systems at the moment, as with all things software, each one wants to be the standard :)

https://jiggerwit.wordpress.com/2018/04/14/the-architecture-...

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

#85

Post by drchewbacca » Tue, Aug 20, 2019, 2:24 PM UTC

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…

Yeah ok when you put it as a bet I think I'll back down ha ha :)

I imagine there will be hold outs who will never switch to formal proofs, though they may simply take on co-authors who are just "formalizers".

I also am probably being over confident with the time scales, I think a process with a tipping point, everyone will use it once everyone starts using it.

However when that tipping point will occur is probably hard to predict. I think it will be soon, but I'm broke and not that sure.