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

81–90 of 112 posts

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

#81

Post by ralph84 »

WCSTombs wrote: post #80

It's easy to forget, as we all use digital tools in our day-to-day lives, that the world is fundamentally analog, and there's no way to escape that. Everyone trying to tell you otherwise is just selling snake oil, with one notable exception , which is mathematical rigor in proofs. It's understood now that a rigorous proof in math is exactly one that, in principle, can be digitized and checked automatically. Those are…

> that the world is fundamentally analog

Isn't that still an unresolved question? Wave-particle duality and all that.

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

#82

Post by cap11235 »

harshreality wrote: post #72
nicoburns wrote: post #67

Earlier quoted context omitted.

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.

Are they bemoaning that science is being done, or are they bemoaning that the experimental results have not yet reached high enough confidence to justify the conclusions being suggested?

More Doctors Smoke Camels!™

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

#83

Post by JumpCrisscross »

harshreality wrote: post #72
nicoburns wrote: post #67

Earlier quoted context omitted.

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.

Are they bemoaning that science is being done, or are they bemoaning that the experimental results have not yet reached high enough confidence to justify the conclusions being suggested?

> Are they bemoaning that science is being done

The reflexive "in mice" comments seem to be bemoaning how science is done.

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

#84

Post by emih »

I like the story in the article, but I think it tries to create some drama where there isn't any.

I think it's great that a lot of work is done using proof assistants, because clearly it's working out for researchers; diversity of research and of methods is a great strength of science. I really can't see how you can "push it too far", pen-and-paper proofs are not going anywhere. And as more researchers write machine-checked proofs, new techniques for automating these proofs are invented (which is what my research is about hehe) which will only make it easier for more researchers to join in.

> Currently, mathematicians are hoping to formalize all of mathematics using a proof assistant called Lean.

_Some_ mathematicians are trying to formalize _some_ of mathematics using a proof assistant called Lean. It's not a new development, proof assistants have been used for decades. Lean 4 has definitely been gaining popularity recently compared to others, but other proof assistants are still very popular.

> a dedicated group of Lean users is responsible for determining which definitions should go into Lean’s library

The article makes it sound like there is a single, universal "The Lean Library" that everyone is restricted to. I assume it refers to mathlib? But at the end of the day it's just code and everyone is writing their own libraries, and they can make their own decisions.

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

#85

Post by seanmcdirmid »

quietbritishjim wrote: post #21
seanmcdirmid wrote: post #20

Earlier quoted context omitted.

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.

I don't think that's true. Often, to come up with a proof of a particular theorem of interest, it's necessary to invent a whole new branch of mathematics that is interesting in its own right e.g. Galois theory for finding roots of polynomials. If the proof is automated then it might not be decomposed in a way that makes some new theory apparent. That's not true of a simple calculation.

> I don't think that's true. Often, to come up with a proof of a particular theorem of interest, it's necessary to invent a whole new branch of mathematics that is interesting in its own right e.g. Galois theory for finding roots of polynomials. If the proof is automated then it might not be decomposed in a way that makes some new theory apparent. That's not true of a simple calculation.

Ya, so? Even if automation is only going to work well on the well understood stuff, mathematicians can still work on mysteries, they will simply have more time and resources to do so.

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

#86

Post by WCSTombs »

ralph84 wrote: post #81
WCSTombs wrote: post #80

It's easy to forget, as we all use digital tools in our day-to-day lives, that the world is fundamentally analog, and there's no way to escape that. Everyone trying to tell you otherwise is just selling snake oil, with one notable exception , which is mathematical rigor in proofs. It's understood now that a rigorous proof in math is exactly one that, in principle, can be digitized and checked automatically. Those are…

> that the world is fundamentally analog Isn't that still an unresolved question? Wave-particle duality and all that.

I think there are some theories that the universe is fundamentally discrete at the lowest level below current capabilities of measurement, but to my knowledge none of those is widely accepted.

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

#87

Post by seanmcdirmid »

jhanschoo wrote: post #30
seanmcdirmid wrote: post #20

Earlier quoted context omitted.

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.

There are areas of mathematics where the standard proofs are very interesting and require insight, often new statements and definitions and theorems for their sake, but the theorems and definitions are banal. For an extreme example, consider Fermat's Last Theorem. Note on the other hand that proving standard properties of many computer programs are frequently just tedious and should be automated.

Yes, but > 90% of the proof work to be done is not that interesting insightful stuff. It is rather pattern matching from existing proofs to find what works for the proof you are currently working on.

If you've ever worked on a proof for formal verification, then its...work...and the nature of the proof probably (most probably) is not going to be something new and interesting for other people to read about, it is just work that you have to do.

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

#88

Post by GuB-42 »

nicoburns wrote: post #67
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.

The problem is more about how it is reported to the public. Science is ugly, but when a discovery is announced to the public, a high level of confidence is expected, and journalists certainly act like there is. Kind of like you are not supposed to ship untested development versions of software to customers.

But sometimes, some of the ugly science gets out of the lab a bit too soon, and it usually doesn't end well. Usually people get their hopes up, and when it doesn't live up to the hype, people get confused.

It really stood out during the covid pandemic. We didn't have time to wait for the long trials we normally expect, waiting could mean thousands of deaths, and we had to make do with uncertainty. That's how we got all sorts of conflicting information and policies that changed all the time. The virus spread by contact, no, it is airborne, masks, no masks, hydroxycholoroquine, no, that's bullshit, etc... that sort of thing. That's the kind of thing that usually don't get publicized outside of scientific papers, but the circumstances made it so that everyone got to see that, including science deniers unfortunately.

Edit: Still, I really enjoyed the LK99 saga (the supposed room temperature superconductor). It was overhyped, and it it came to its expected conclusion (it isn't), however, it sparked widespread interest in semiconductors and plenty of replication attempts.

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

#89

Post by pfdietz »

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.

Of course, once LLMs are really good at that, they can be set loose on the entire historical math literature, all 3.5M papers worth. And then LLMs can be trained on these formalized results (the ones that turn out upon attempted formalization to have been correct.)

How good do you think AI will be at proving new results given that training set?

Math is going to change, and change massively. There's a lot of whistling past the graveyard going on from those who are frightened by this prospect.

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

#90

Post by dyauspitr »

nicoburns wrote: post #67
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.

It depends, especially coming from fields like psychology. You can prove anything with a small enough group. A lot of those just end up adding a lot of noise and reduce the reliability of the entire field in general. It just ends up with people getting conflicting information every other week and then they just tune out.
Post reply on HN