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

In math, rigor is vital, but are digitized proofs taking it too far?

quantamagazine.org

Post reply on HN
Print view View original

11–20 of 112 posts

Re: In math, rigor is vital, but are digitized proofs taking it too far?

#11

Post by coldcity_again »

pavpanchekha wrote: post #10
johnbender wrote: post #4

I’m confused by the calculus example and I’m hoping someone here can clarify why one can’t state the needed assumptions for roughed out theory that still need to be proven? That is, I’m curious if the critical concern the article is highlighting the requirement to “prove all assumptions before use” or instead the idea that sometimes we can’t even define the blind spots as assumptions in a theory before we use it?

In calculus the core issue is that the concept of a "function" was undefined but generally understood to be something like what we'd call today an "expression" in a programming language. So, for example, "x^2 + 1" was widely agreed to be a function, but "if x The formal definition of "function" is totally different! This is typically a big confusion in Calculus 2 or 3! Today, a function is defined as literally any in…

That's very helpful and clear, thank you

Re: In math, rigor is vital, but are digitized proofs taking it too far?

#12

Post by gzread »

riverforest wrote: post #3

Rigor is the whole point of math. The moment you start asking if there is too much of it you are solving a different problem.

It seems you have never tried to prove anything using a proof assistant program. It will demand proofs for things like x x<z and while it should have that built in for natural numbers, woe fall upon thee who defines a new data type.

Re: In math, rigor is vital, but are digitized proofs taking it too far?

#13

Post by cbdumas »

storus wrote: post #8
riverforest wrote: post #3

Rigor is the whole point of math. The moment you start asking if there is too much of it you are solving a different problem.

Rigor is one solution to mutual understanding Bourbaki came up with that in turn led to making math inaccessible to most humans as it now takes regular mathematicians over 40 years to get to the bleeding edge, often surpassing their brain's capacity to come up with revolutionary insights. It's like math was forced to run on assembly language despite there were more high-level languages available and more apt for the…

> It's like math was forced to run on assembly language despite there were more high-level languages available and more apt for the job.

I'm not a mathematician but that doesn't sound right to me. Most math I did in school is comprised concepts many many layers of abstraction away from its foundations. What did you mean by this?

Re: In math, rigor is vital, but are digitized proofs taking it too far?

#15

Post by YetAnotherNick »

umutisik wrote: post #9

With sufficient automation, there shouldn't really be a trade-off between rigor and anything else. The goal should be to automate as much as possible so that whatever well-defined useful thing can come out theory can come out faster and more easily. Formal proofs make sense as part of this goal.

The thing is if something is proved by checking million different cases automatically, it makes it hard to factor in learning for other proofs.

Re: In math, rigor is vital, but are digitized proofs taking it too far?

#16

Post by storus »

cbdumas wrote: post #13
storus wrote: post #8

Earlier quoted context omitted.

Rigor is one solution to mutual understanding Bourbaki came up with that in turn led to making math inaccessible to most humans as it now takes regular mathematicians over 40 years to get to the bleeding edge, often surpassing their brain's capacity to come up with revolutionary insights. It's like math was forced to run on assembly language despite there were more high-level languages available and more apt for the…

> It's like math was forced to run on assembly language despite there were more high-level languages available and more apt for the job. I'm not a mathematician but that doesn't sound right to me. Most math I did in school is comprised concepts many many layers of abstraction away from its foundations. What did you mean by this?

My math classes were theorem, lemma, proof all day long, no conceptualization, no explanation; low-level formulas down to axioms. Sink or swim, figure it out on your own or fail.

Re: In math, rigor is vital, but are digitized proofs taking it too far?

#17

Post by 1970-01-01 »

woopwoop wrote: post #7
riverforest wrote: post #3

Rigor is the whole point of math. The moment you start asking if there is too much of it you are solving a different problem.

Rigor is not the whole point of math. Understanding is. Rigor is a tool for producing understanding. For a further articulation of this point, see https://arxiv.org/abs/math/9404236

This conflates rigor with proof. Proof is the solve to the argument you are making. Rigor is how carefully and correctly the argument is made. You can understand something without rigor but you cannot prove it.

Re: In math, rigor is vital, but are digitized proofs taking it too far?

#18

Post by storus »

umutisik wrote: post #9

With sufficient automation, there shouldn't really be a trade-off between rigor and anything else. The goal should be to automate as much as possible so that whatever well-defined useful thing can come out theory can come out faster and more easily. Formal proofs make sense as part of this goal.

There are still many major oversimplifications in the core of math, making it weirdly corresponding with the real world. For example, if you want to model human reasoning you need to step away from binary logic that uses "weird" material implication that is a neat shortcut for math to allow its formalization but doesn't map well to reasoning. Then you might find out that e.g. medicine uses counterfactuals instead of material implication. Logics that tried to make implication more "reasonable" like relevance logic are too weak to allow formalization of math. So you either decide to treat material implication as correct (getting incompleteness theorem in the end), making you sound autistic among other humans, or you can't really do rigorous math.

Re: In math, rigor is vital, but are digitized proofs taking it too far?

#19

Post by _alternator_ »

umutisik wrote: post #9

With sufficient automation, there shouldn't really be a trade-off between rigor and anything else. The goal should be to automate as much as possible so that whatever well-defined useful thing can come out theory can come out faster and more easily. Formal proofs make sense as part of this goal.

Let’s not forget that mathematics is a social construct as much as (and perhaps more than) a true science. It’s about techniques, stories, relationships between ideas, and ultimately, it’s a social endeavor that involves curiosity satisfaction for (somewhat pedantic) people. If we automate ‘all’ of mathematics, then we’ve removed the people from it.

There are things that need to be done by humans to make it meaningful and worthwhile. I’m not saying that automation won’t make us more able to satisfy our intellectual curiosity, but we can’t offload everything and have something of value that we could rightly call ‘mathematics’.

Re: In math, rigor is vital, but are digitized proofs taking it too far?

#20

Post by seanmcdirmid »

_alternator_ wrote: post #19
umutisik wrote: post #9

With sufficient automation, there shouldn't really be a trade-off between rigor and anything else. The goal should be to automate as much as possible so that whatever well-defined useful thing can come out theory can come out faster and more easily. Formal proofs make sense as part of this goal.

Let’s not forget that mathematics is a social construct as much as (and perhaps more than) a true science. It’s about techniques, stories, relationships between ideas, and ultimately, it’s a social endeavor that involves curiosity satisfaction for (somewhat pedantic) people. If we automate ‘all’ of mathematics, then we’ve removed the people from it. There are things that need to be done by humans to make it meaningfu…

Automating proofs is like automating calculations: neither is what math is, they are just things in the way that need to be done in the process of doing math.

Mathematicians will just adopt the tools and use them to get even more math done.

Post reply on HN