In math, rigor is vital, but are digitized proofs taking it too far? • Hacker News Board

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

#101

Post by alde » Tue, Mar 31, 2026, 1:32 AM UTC

deterministic wrote: post #96

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

There is no such evidence. The widely accepted models of physics are all continuous. If you see headlines like "physicists think our world might be discrete" please read them as "scientists cured cancer in mice".

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

#102

Post by potsandpans » Tue, Mar 31, 2026, 1:38 AM UTC

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.

Like anything else, it's easier to complain about the legitimacy of something and nitpick it to death than it is to do the actual thing.

Most people on HN aren't scientists, even if they fancy themselves as such.

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

#103

Post by cwillu » Tue, Mar 31, 2026, 2:25 AM UTC

JumpCrisscross wrote: post #100

cwillu wrote: post #98

Earlier quoted context omitted.

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.

Dismissing good science is entirely the correct decision when the good science isn't ready for broad dissemination to the audience which it is being presented to.

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

#104

Post by nimish » Tue, Mar 31, 2026, 2:40 AM UTC

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…

We already have had that ossified layer thing multiple times in mathematics. Formalisms change. For example, prior to vector calculus writing out multidimensional PDEs was tedious. Vector calculus has serious issues in its own right, so you get people pushing geometric algebra. In more rarefied domains you have things like categories and sheafs replacing the previous "ossified" layer.

It'll keep going on and on.

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

#105

Post by Someone » Tue, Mar 31, 2026, 7:26 AM UTC

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…

> 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 Good answer, but not the best example. In many programming languages, the latter is easily written as an expression:

   (x - abs(x)) / 2

It boils down to what you call an elementary function (https://en.wikipedia.org/wiki/Elementary_function).

Taking the absolute of a number generally is not assumed to be in that set, but there is no generally accepted strict definition.

A step ‘up’ from elementary functions are special functions (https://en.wikipedia.org/wiki/Special_functions). Likewise, that is loosely defined.

For example https://en.wikipedia.org/wiki/List_of_eponyms_of_special_fun... mentions lots of polynomials, one of them https://en.wikipedia.org/wiki/Cyclotomic_polynomial, which definitely are elementary according to https://en.wikipedia.org/wiki/Elementary_function.

Wikipedia also contradicts itself in https://en.wikipedia.org/wiki/Closed-form_expression, where it says

“a closed form expression or formula is one that is formed with constants, variables, and a set of functions considered as basic and connected by arithmetic operations (+, −, ×, /, and integer powers) and function composition. Commonly, the basic functions that are allowed in closed forms are nth root, exponential function, logarithm, and trigonometric functions”

and

“For example, if one adds polynomial roots to the basic functions, the functions that have a closed form are called elementary functions”

That would put the goniometric functions in the basic set allowed in elementary functions.

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

#106

Post by meroes » Tue, Mar 31, 2026, 9:02 AM UTC

SabrinaJewson wrote: post #59

meroes wrote: post #5

Earlier quoted context omitted.

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.

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

#107

Post by nathan_compton » Tue, Mar 31, 2026, 11:26 AM UTC

sesm wrote: post #58

justonceokay wrote: post #32

Earlier quoted context omitted.

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

Sounds lame and boring to me.

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

#108

Post by dyauspitr » Tue, Mar 31, 2026, 5:27 PM UTC

JumpCrisscross wrote: post #97

dyauspitr wrote: post #91

Earlier quoted context omitted.

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.

I’m not advocating for censoring them. I’m advocating for less hype in science media reporting around mice studies because let’s be frank. The vast majority of the population are ignoramuses that cannot make the distinctions themselves, and that has real political consequences through lack of trust in scientific organizations.

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

#109

Post by raincom » Tue, Mar 31, 2026, 6:16 PM UTC

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…

That’s similar to Neurath’s boat:” We are like sailors who on the open sea must reconstruct their ship but are never able to start afresh from the bottom. Where a beam is taken away a new one must at once be put there, and for this the rest of the ship is used as support. In this way, by using the old beams and driftwood the ship can be shaped entirely anew, but only by gradual reconstruction.”

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

#110

Post by ndriscoll » Tue, Mar 31, 2026, 10:32 PM UTC

integralid wrote: post #49

ndriscoll wrote: post #29

Earlier quoted context omitted.

This is literally the same thing as having the model write well factored, readable code. You can tell it to do things like avoid mixing abstraction levels within a function/proof, create interfaces (definitions/axioms) for useful ideas, etc. You can also work with it interactively (this is how I work with programming), so you can ask it to factor things in the way you prefer on the fly.

>This is literally the same thing as No. >You can Not right now, right? I don't think current AI automated proofs are smart enough to introduce nontrivial abstractions. Anyway I think you're missing the point of parent's posts. Math is not proofs. Back then some time ago four color theorem "proof" was very controversial, because it was a computer assisted exhaustive check of every possibility, impossible to verify by…

Right, in the same way that programs are not opcodes. They're written to be read and understood by people. Language models can deal with this.

I'm not sure what your threshold for "trivial" is (e.g. would inventing groups from nothing be trivial? Would figuring out what various definitions in condensed mathematics "must be" to establish a correspondence with existing theory be trivial?), but I see LLMs come up with their own reasonable abstractions/interfaces just fine.