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

(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

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.

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.

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

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.

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.

Sadly not sometimes it is just:

computer says

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

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

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.

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

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.