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?

#71

Post by segfaultbuserr » Mon, Aug 19, 2019, 8:42 AM UTC

whatshisface wrote: post #53

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…

I wonder what fraction of web programmers understand transistor physics?

> what fraction of web programmers understand transistor physics?

I'm not an engineer, but I imagine that even most professional electrical/electronic engineers do not understand transistor physics in full details. In engineering, a transistor is essentially treated as a blackbox, and its behavior is described and approximated by various small-signal and large-signal models (i.e. treated as a lumped component), with their parameters characterized empirically by vendors through experiments. How exactly things work at atomic or quantum level is essentially for a transistor to work, yet, a subject of study unrelated to electrical engineering.

On the other hand, I imagine there is no shortage of EEs who have studied a physics major, or EEs with a background of semiconductor physics - they can understand transistor physics really well.

So we can say the relation between EE and transistor physics sounds a lot similar to mathematicians and logicians, it's a good analogy.

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

#72

Post by segfaultbuserr » Mon, Aug 19, 2019, 8:52 AM UTC

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 heard that the outputs of formal verification tools are often unreadable, as they work through the proof mechanically, step-by-step. It means sometimes the computer can tell if the reasoning is flawed, but it takes a lot of effort to understand the counter-argument from the computer. Is there any effort to solve this problem?

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

#73

Post by jokoon » Mon, Aug 19, 2019, 10:35 AM UTC

alanbernstein wrote: post #62

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.

Not saying it's not fun, but to me proofs don't seem to help me understanding mathematics.

Not saying proofs are not important, but it seems that proving a theorem is important at a higher levels of mathematics, not in high school or university.

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

#74

Post by waterhouse » Mon, Aug 19, 2019, 11:48 AM UTC

codesushi42 wrote: post #26

paulpauper wrote: post #18

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

While we're on the subject:

The engineer thinks his equations approximate reality. The physicist thinks reality approximates his equations. The mathematician doesn't care.

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

#75

Post by [deleted] » Mon, Aug 19, 2019, 12:24 PM UTC

perl4ever wrote: post #57

krastanov wrote: post #40

Earlier quoted context omitted.

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

"The unreasonable effectiveness of mathematics" just always struck me as similar to commenting on how noses are made to fit glasses.

[deleted]

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

#76

Post by blt » Mon, Aug 19, 2019, 12:27 PM UTC

alexmlamb wrote: post #67

galaxyLogic wrote: post #38

Earlier quoted context omitted.

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

Right, it's possible to get to LA's airport with public transit, but the amount of time it takes cannot be upper bounded using currently known techniques.

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

#77

Post by robpal » Mon, Aug 19, 2019, 1:28 PM UTC

Pretty funny to see Simpson's name showing up here. I have kept two souvenirs from my academic life: the original manuscript of my thesis and Simpson's very eloquent and overwhelmingly positive review of it.

Regarding the topic, I'd say that mathematics, as a whole, is a set of intuitions and ideas, rather than strict proofs. I've spent a fair amount of time working my way through some of Kontsevich's ideas and attended many of his talks -- he rarely (if ever) gives any proofs, my educated guess is that he proposes some extremely profound ideas and his collaborators grind through the details (not always). And it still works just fine.

I remember Kenji Fukaya saying once, talking about a PDE-heavy theorem: "We are trying to keep the details of the proof under 500 pages and it's not sa easy". The main issue here is that people who don't do professional, academic research in mathematics are unaware of the complexity of modern maths. It has evolved immensely during last 50 years, the theories are just layers and layers of foundational work one has to assimilate before getting any work done. Rigorous verification takes years and no one in the academia is being offered a job for proof-reading of existing papers.

One should also remember that referees of the papers are not being paid, it's considered "work for the community" and it's hard to blame them for not reading the papers in detail.

Mathematics are anti-fragile.

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

#78

Post by 0815test » Mon, Aug 19, 2019, 3:19 PM UTC

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…

> I am sure within 10 years every professional mathematician will use formal proofs.

They said the exact same thing 10 years ago - see e.g. https://www.vdash.org and the AMS Notices special issue on formal proof from around the same timeframe. Formal proofs are hard, sometimes tedious and not always very intuitive. They're slowly spreading out from the most "synthetic" subfields of math (the ones where you're basically working with unfamiliar "rules", but not with a huge library of proven results), but progress is really slow - definitely slower than many people would expect!

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

#79

Post by philipov » Mon, Aug 19, 2019, 11:31 PM UTC

dwohnitmok wrote: post #65

dwohnitmok wrote: post #52

Earlier quoted context omitted.

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

I have a general algebra textbook that uses category theory as a foundation, and although I haven't gotten very far into it, my impression is that either category theory or ZFC can be used to derive the other one. As a result, it doesn't matter a whole lot where you start since you get both eventually anyway. If category theory adds tools that make it easier to prove theorems, that's great and useful, but no one really cares if it was foundational or derived.

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

#80

Post by dwohnitmok » Tue, Aug 20, 2019, 12:23 AM UTC

philipov wrote: post #79

dwohnitmok wrote: post #65

Earlier quoted context omitted.

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

I have a general algebra textbook that uses category theory as a foundation, and although I haven't gotten very far into it, my impression is that either category theory or ZFC can be used to derive the other one. As a result, it doesn't matter a whole lot where you start since you get both eventually anyway. If category theory adds tools that make it easier to prove theorems, that's great and useful, but no one real…

This is one main reason why the larger mathematical community does not closely follow these foundational discussions (there are foundations that are strict extensions of ZFC but these extensions are usually conservative).

The usual response is that it would be nice if the formal foundations of mathematics corresponded more closely to the informal intuitions of mathematicians, which is arguably not true of set theoretic foundations and perhaps is more true of category theory. Whether or not you agree about the correspondence or whether even if you agree you find it at all convincing is up to you.