Hacker News Reader

Comment by riverforest | Hacker News Reader

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.

View on HN

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.

> You can understand something without rigor but you cannot prove it.

I think I disagree. There are formal proofs and informal proofs, there are rigorous proofs and less rigorous proofs. Of course, a rigorous proof requires rigor, but that’s close to tautological. What makes a proof is that it convinces other people that the consequent is true. Rigor isn’t a necessary condition for that.

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

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

If rigor is the whole point why are we so focused on classical math (eg classical logic) not the wider plurality?

How does that relate at all? Classical logic is not any less rigorous than other kinds of logic.

Because if rigor is all we cared about I’d think we’d spend more time on non-classical math.

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

Reply on news.ycombinator.com