Live data from Hacker News

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

quantamagazine.org

91–100 of 112 posts

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

#91

Earlier quoted context omitted.

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.

I disagree. I think people understand studies have to begin in mice. It’s what the GP said. You can’t release those studies because there’s not a high enough confidence rate in what most people are interested in ie how it effect humans.

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

#92
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…

Maths doesn't need a litus test, because its not chemistry. You mentioned ideas being ossified and that might be one of them.

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

#93
post #88

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.

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

  > The problem is more about how it is reported to the public. 
Yes and no.

From scientific communicators there's a lot of slop and it's getting worse. Even places like Nature and Scientific American are making unacceptable mistakes (a famous one being the quantum machine learning black hole BS that Quanta published)

But I frequently see those HN comments on ArXiv links. That's not a science communication issue. Those are papers. That's researcher to researcher communication. It's open, but not written for the public. People will argue it should be, but then where does researcher to researcher communication happen? You really want that behind closed doors?

There is a certain arrogance that plays a role. Small sample size? There's a good chance it's a paper arguing for the community to study at a larger scale. You're not going to start out by recruiting a million people to figure out if an effect might even exist. Yet I see those papers routinely scoffed at. They're scientifically sound but laughing at them is as big of an error as treating them like absolute truth, just erring in the opposite direction.

People really do not understand how science works and they get extremely upset if you suggest otherwise. As if not understanding something that they haven't spent decades studying implies they're dumb. Scientists don't expect non scientists to understand how science works. There's a reason you're only a junior scientist after getting an entire PhD. You can be smart and not understand tons of stuff. I got a PhD and I'll happily say I'll look like a bumbling idiots even outside my niche, in my own domain! I think we're just got to stop trying to prove how smart we are before we're all dumb as shit. We're just kinda not dumb at some things, and that's perfectly okay. Learning is the interesting part. And it's extra ironic the Less Wrong crowd doesn't take those words to heart because that's what it's all about. We're all wrong. It's not about being right, it's about being less wrong

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

#94
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…

[dead]

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

#95
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…

> someone wins a Fields using a proof-assistant in an essential way.

Terence Tao is actively using LEAN and working with the LEAN community to prove leading edge mathematics.

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

#96

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

Whether the world is discrete or analog is still an open problem in science. And it looks as if there is more and more evidence that the world is actually discrete at the quantum level.

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

#97

Earlier quoted context omitted.

> Are they bemoaning that science is being done The reflexive "in mice" comments seem to be bemoaning how science is done.

I disagree. I think people understand studies have to begin in mice. It’s what the GP said. You can’t release those studies because there’s not a high enough confidence rate in what most people are interested in ie how it effect humans.

> You can’t release those studies because there’s not a high enough confidence rate in what most people are interested in ie how it effect humans

This is science by ignoramus. It isn't how science works, at least not when it works at its best. Someone advocating for censoring science because it might be misread is not on the side of science.

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

#98

Earlier quoted context omitted.

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.

As someone who has made several comments consisting entirely of “…in mice.”, let me assure you that the reflex only kicks in after reading the paper and noticing that the experimental subjects were exclusively mice.

The problem is not mice experiments on arxiv, the problem is posting those papers for broader dissemenation to the public, with titles suggesting to the public that cancer has been cured, without prominently pointing out that the experiments were not about cancer in humans.

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

#99

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

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…

Exactly. The reason mathematicians and physicists care about elegance is because they care about understanding things. Elegance, like you said, isn't about aesthetics, even though people seem to think they're synonymous. But the elegance is that you've reduced things to simple components. That not only makes it easier for us humans to understand but it means you're closer to the minimal structure. Meaning you know what matters and more importantly, what doesn't.

Tbh, elegance is something programmers should strive for too. Elegant code is easier to build upon, easier to read/understand, easier to modify, easier to adapt. For all the same reasons mathematicians want elegance. Though it's true for many domains. People love to throw around the term "first principles" but that's not something you (usually) start at, that's something you derive. And it's usually not very easy to figure out

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

#100
post #98

Earlier quoted context omitted.

> Are they bemoaning that science is being done The reflexive "in mice" comments seem to be bemoaning how science is done.

As someone who has made several comments consisting entirely of “…in mice.”, let me assure you that the reflex only kicks in after reading the paper and noticing that the experimental subjects were exclusively mice. The problem is not mice experiments on arxiv, the problem is posting those papers for broader dissemenation to the public, with titles suggesting to the public that cancer has been cured, without prominen…

> problem is posting those papers for broader dissemenation to the public, with titles suggesting to the public that cancer has been cured

Fair enough. I'm thinking of cases where a good study that isn't turned into PR slop is dismissed because it was done in mice. Which is fine for most people. But not great if we're treating real science that way.

Post reply on HN