Hacker News Reader

Comment by zitterbewegung | Hacker News Reader

Math doesn’t have a replication crisis at all it has a comprehension crisis.

Since proofs are programs one can basically say that mathematical theorems are incredibly detailed software that is completely open source and invites people to identify programs that don’t work and or fix issues.

A famous one is Fermats last theorem which needed a fix but was largely right.

Others have said that it takes 6 months to a year to get published. The other thing with math is the fact that you can get completely scooped and your work is worthless.

Edit: I am using "proofs are programs" very loosely and yes Theorems are much more than programs as other commenters have pointed out.

View on HN

A more notorious example of the comprehension crisis would be Mochizuki's claimed proof of the abc conjecture. So far fairly few people are willing to claim they both understand and agree with the several hundred pages of 'proof'.

https://en.wikipedia.org/wiki/Shinichi_Mochizuki

It's a fun rabbit hole to go down :)

I was tempted to use that but Fermat's last theorem is known to the general public for much longer and has a resolution.

It was a good example, and definitely one of the more important examples of how finding and fixing mistakes in mathematics is supposed to happen. I figured the abc-conjecture would provide a nice contrasting example.

The math department at my university tried to read through the proof of Fermat's last theorem, as a for-fun activity. They eventually gave up because they realized it would take too much time.

Interesting! My experience is that scooping is less of an issue in math than in any of the science fields I have friends in. Papers are lower-stakes, there's less money involved, and if two of you are working on the same project you can just co-author.

(And if you have an independent paper, that can _also_ get published; your paper is distinct even if the result isn't. I think the PT HOMFLY polynomial was independently proven in like four different papers published within two years (and it's named so that all eight authors get credit).

But also, publication lags shouldn't lead to more scooping, because you can put it up on the arXiv at the beginning of the publication process, not the end. In my experience the paper is treated as "real" once it hits the arXiv; the acceptance is mostly a formality that lets us put it on our promotion packet.

But also, publication times don't lead to scooping generally because you

> Since proofs are programs one can basically say that mathematical theorems are incredibly detailed software that is completely open source and invites people to identify programs that don’t work and or fix issues.

I don't think it's that straightforward; proofs in papers are a mix between explanation in natural language and mechanical steps. Not every step of deduction can feasibly be written out. That's part of why computer aided proofs are not that popular in math.

Having a paper published can take a very very long time, a year is quite short and 6 months is basically the minimum wait. My last paper has taken 2 years to be accepted from the first time I submitted it, despite it being largely the same as the initial submission, accepted as part of my thesis over a year ago, and having several citations. It is very frustrating, and it also means that easier (and less original) work is easier to publish.

An interesting perspective on programs-as-proof is I-forget-his-name-but... the mathematician who made really bold claims, if only you'd study under his tutelage for a number of years to understand this whole new terminology he invented.

With programs-as-proof it really wouldn't matter. It's either "computer says yes" or "compu'er says noooo".

EDIT: Whoop, sibling post mentioned, it's Mochizuki.

This doesn't seem a very generous description of Mochizuki's work. You don't "need" to study under him for a number of years and there's no evidence he's being obscurantist. The proof is long and has a lot of novel techniques he's invented, and he works primarily in Japanese. You can reasonably side with e.g. Scholze's interpretation without thinking Mochizuki is disingenuous or some kind of scammer.

He's considerably less esoteric than e.g. Grothendieck was even during his more "public" years.

I have nothing invested in whether or not any given mathematician is right or wrong. I just picked a random example of a controversial proof -- the point was more that proof-as-computation could settle and any all disputes.

It might not lend more understanding to people not invested in "field X" (or even people who are invested in field X!), but it would be proof.

Proof in the current world of math is quite intangible.

I think the demand for "tangible" proof (if by that you mean, fully mechanically-verifiable proofs and a style unlike anything common in mathematics papers today) is a bit silly and seems to be driven by some ideologies well outside of mathematics, rather than mathematicians themselves.

A proof is whatever convinces sufficient mathematicians that the theorem is consequent! Classical logical systems are a very good way to do that so they get used a lot. But they're not the only way, and involving a computer program makes most proofs less convincing rather than more.

> It's either "computer says yes" or "compu'er says noooo".

Sadly not sometimes it is just:

computer says

Or "computer says x but you don't trust the hardware/software".

Or "computer says x but you don't agree the mathematical concept was correctly formalized into the proof engine language".

> The other thing with math is the fact that you can get completely scooped and your work is worthless

Why math specifically? One would think this applies in virtually all fields.

Increase in development time (publication can take 6 months to a year).

I would say its more like pseudocode. There can be quite a large gap between a normal proof, and a machine checkable proof, which is the computer program version.

Aren't programs generally more complex than math proofs?

Like, the more accidental edge cases people produce, the less they understand the program.

Not any proof with quantifiers. As soon as statement contains ∀ (for all) ∃ (there exists one) where you have a way bigger branching factor and the claim after the quantifiers needs to be true all for all (or atleast for one) element of the set you draw from.

Yes, what I meant was, math proofs are well defined, and programs are often a heap of stuff thrown together.

While it's harder to produce the math proof, it's probably harder to grasp what's going on in a program in a mathematical sense.

Reply on news.ycombinator.com