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

61–70 of 112 posts

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

#61

Post by pas »

dooglius wrote: post #40
msteffen wrote: post #39

Earlier quoted context omitted.

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

Agreed; e.g. if you prove something about the real numbers, the matter of how R is constructed out of your axiomatic system doesn't matter

there are questions where the abstraction of real numbers becomes leaky, and some axioms (or their lack) poke through.

https://en.wikipedia.org/wiki/Axiom_of_choice#Real_numbers

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

#62

Post by jojomodding »

storus wrote: post #18
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…

People keep getting hung up on material implication but it can not understand why. It's more than an encoding hack--falsity (i.e. the atomic logical statement equivalent to 0=1) indicates that a particular case is unreachable and falsity elimination (aka "from falsity follows everything") expresses that you have reached such a case as part of the case distinctions happening in every proof.

Or more poetically, "if my grandmother had wheels she would have been a bike[1]" is a folk wisdom precisely because it makes so much sense.

1: https://www.youtube.com/watch?v=A-RfHC91Ewc

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

#63

Post by zarzavat »

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

I know what you're saying but elegance is not simply an aesthetic concern.

The value of a proof is not only its conclusion but also the insight that it provides through its method.

The goal of mathematics is not to prove as many theorems as possible but rather to gain an ever deeper understanding of why certain statements are true. The way that something is proved can be more or less useful to advancing that goal.

As an example the elementary proof(s) of the prime number theorem are just about as famous as the original proof. Sometimes the second bite of the cherry is even juicier than the first.

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

#64

Post by ratmice »

WhitneyLand wrote: post #51

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

My only complaint with the article is that it doesn't seem to mention that digitized proofs can contain gaps but that those gaps must be explicit like in lean the `sorry` function, or axioms.

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

#65

Post by jfarmer »

dooglius wrote: post #40
msteffen wrote: post #39

Earlier quoted context omitted.

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

Agreed; e.g. if you prove something about the real numbers, the matter of how R is constructed out of your axiomatic system doesn't matter

The picture isn't quite so clean in the constructive context, which is what many of these proof systems are rooted in, e.g., https://mathoverflow.net/questions/236483/difference-between...

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

#66

Post by auntienomen »

fasterik wrote: post #56
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.

Exactly this. LLMs really aren't built for discovering new mathematics, especially _interesting_ new mathematics. They're built to try the most obvious patterns. When that works, it's pretty much by definition not interesting.

What LLMs are good at is organizing concepts, filling in detail, and remembering to check corner cases. So their use should help mathematicians to get a better handle on what's terra firma and what's still exploration. Which is great. Proof by it-convinced-other-mathematicians doesn't have a flawless track record. Sometimes major theorems turn out to be wrong or wrong-as-stated. Sometimes they're right, but there's never been a complete or completely correct proof in the literature. The latter case is actually quite common, and formal proof is just what's needed.

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

#67

Post by nicoburns »

WhitneyLand wrote: post #51

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

Yeah, I see a lot of people (especially on HN) bemoaning any science that isn't a controlled double blind experiment with a large sample size. But exploratory science is just as important as the science that proves things. Otherwise we wouldn't know which hypotheses are useful/interesting to test.

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

#68

Post by zozbot234 »

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…

> however what happens is that, as in software, certain ideas get ossified. That’s why, for example, every OS has a POSIX layer

Refactoring formalized developments is vastly easier than refactoring software or informal math, since you get verified feedback as to whether the refactoring is correct.

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

#69

Post by zozbot234 »

auntienomen wrote: post #66
fasterik wrote: post #56

Earlier quoted context omitted.

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

Exactly this. LLMs really aren't built for discovering new mathematics, especially _interesting_ new mathematics. They're built to try the most obvious patterns. When that works, it's pretty much by definition not interesting. What LLMs are good at is organizing concepts, filling in detail, and remembering to check corner cases. So their use should help mathematicians to get a better handle on what's terra firma and…

LLMs and interactive theorem provers are vastly different. There are AI models that come up with workable formal proofs for ITPs but these aren't your usual frontier models, they're specifically trained for this task.

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

#70

Post by anthk »

integralid wrote: post #50
anthk wrote: post #46

Earlier quoted context omitted.

[flagged]

First of all, I think your comment is against HN guidelines. And I expect GP has actually a lot of experience in mathematics - there are exactly right and this is how professional mathematicians see math (at least most of them, including ones I interact with).

Engineers, maybe. Not the case with Mathematicians.
Post reply on HN