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

51–60 of 112 posts

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

#51

Post by WhitneyLand »

Great quote from Hilbert, I think it’s also a useful thought for software development.

“The edifice of science is not raised like a dwelling, in which the foundations are first firmly laid and only then one proceeds to construct and to enlarge the rooms,” the great mathematician David Hilbert wrote in 1905 (opens a new tab). Rather, scientists should first find “comfortable spaces to wander around and only subsequently, when signs appear here and there that the loose foundations are not able to sustain the expansion of the rooms, [should they] support and fortify them.”

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

#52

Post by enricozb »

msteffen wrote: post #39
sxzygz wrote: post #35

The problem with this ambition is that it turns mathematics into software development. There’s absolutely nothing wrong with this per se, however what happens is that, as in software, certain ideas get ossified. That’s why, for example, every OS has a POSIX layer even though technically the process/namespace/security model could be radically reimagined possibly to create more easily engineered, correct software. Math…

> what happens is that, as in software, certain ideas get ossified. That’s why, for example, every OS has a POSIX layer even though technically the process/namespace/security model could be radically reimagined possibly to create more easily engineered, correct software. Total amateur here, but it strikes me that one important difference is that performance matters in software in a way that it doesn’t in mathematics—…

Proof irrelevance I don't think is accepted in constructivist situations. Those are, however, not that relevant to the recent wave of AI math which uses Lean, whose type system includes classical mathematics.

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

#53

Post by perching_aix »

sxzygz wrote: post #35

The problem with this ambition is that it turns mathematics into software development. There’s absolutely nothing wrong with this per se, however what happens is that, as in software, certain ideas get ossified. That’s why, for example, every OS has a POSIX layer even though technically the process/namespace/security model could be radically reimagined possibly to create more easily engineered, correct software. Math…

Haven't science and mathematics always worked like this? Models are built, they ossify, and eventually get replaced when they become limiting. Software just makes that process more explicit. Or at least I don't see how math turning into software development would selectively promote this effect.

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

#54

Post by SabrinaJewson »

adrianN wrote: post #44
_alternator_ wrote: post #19

Earlier quoted context omitted.

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…

There is a bit about this in Greg Egan‘s Disspora, where a parallel is drawn between maths and art. It is not difficult to automate art in the sense that you can enumerate all possible pictures, but it takes sentient input to find the beautiful areas in the problem space.

I do not think this parallel works, because I think you would struggle to find a discipline for which this is not the case. It is trivial to enumerate all the possible scientific or historical hypothesis, or all the possible building blueprints, or all the possible programs, or all the possible recipes, or legal arguments…

The fact that the domain of study is countable and computable is obvious because humans can’t really study uncountable or uncomputable things. The process of doing anything at all can always be thought of as narrowing down a large space, but this doesn’t provide more insight than the view that it’s building things up.

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

#55

Post by casey2 »

In the long run creating a certificate that guarantees a certain probability of correctness will take much less energy. Right now we can run miller-rabin and show with 1-(1/10^100) certainty that the number is/isn't prime. Similar for hash collisions, after a certain point these can't happen in reality. If Anthropic can get their uptime from 1 9 to 9 9s (software isn't the bottleneck for 9 9s) then we don't need formally checked proofs.

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

#56

Post by fasterik »

sxzygz wrote: post #35

The problem with this ambition is that it turns mathematics into software development. There’s absolutely nothing wrong with this per se, however what happens is that, as in software, certain ideas get ossified. That’s why, for example, every OS has a POSIX layer even though technically the process/namespace/security model could be radically reimagined possibly to create more easily engineered, correct software. Math…

>The litmus test will be when, if ever, someone wins a Fields using a proof-assistant in an essential way.

You're assuming that the point of interactive theorem provers is to discover new mathematics. While that's an interesting research area, it seems like the more practical application is verifying proofs one has already discovered through other means.

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

#57

Post by fasterik »

tines wrote: post #23
jl6 wrote: post #22

Imagine a future where proofs are discovered autonomously and proved rigorously by machines, and the work of the human mathematician becomes to articulate the most compelling motivations, the clearest explanations, and the most useful maps between intuitions, theorems, and applications. Mathematicians as illuminators and bards of their craft.

But in this future, why will “the most compelling motivations, the clearest explanations, and the most useful maps between intuitions, theorems, and applications” be necessary? Catering to hobbyists?

Most mathematicians don't understand the fields outside of their specialization (at a research level). Your assumption that intuition and applications are limited to hobbyists ignores the possibility of enabling mathematicians to work and collaborate more effectively at the cutting edge of multiple fields.

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

#58

Post by sesm »

justonceokay wrote: post #32
_alternator_ wrote: post #19

Earlier quoted context omitted.

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…

> mathematics is a social construct If you believe Wittgenstein then all of math is more and more complicated stories amounting to 1=1. Like a ribbon that we figure out how to tie in ever more beautiful knots. These stories are extremely valuable and useful, because we find equivalents of these knots in nature—but boiled down that is what we do when we do math

In my view mathematics builds tools that help solve problems in science.

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

#59

Post by SabrinaJewson »

meroes wrote: post #5
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.

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.

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

#60

Post by lilyball »

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…

> If you formalize, you'll end up with one rigorous definition

Can't you just formalize both definitions and pick the one to work with based on what you want to do? Surely the only obstacle here is the time and effort it takes to write the formalization?

Or, alternatively, just because you've formalized the advanced calculus version doesn't mean you need to use the formalization when teaching basic calculus. The way we've proven something and the way we teach that something don't have to be the same.

Post reply on HN