logoalt Hacker News

impendiayesterday at 7:14 PM1 replyview on HN

Mathematician here. There is a lot of recent work on the Lean project -- when a proof can be translated into Lean code, then it can be strictly and formally validated.

https://lean-lang.org/

But otherwise, mathematical proofs are read and written by humans, and at the end of the day the relevant standard of proof is what other mathematicians will accept.

Occasionally, mathematicians don't agree. For a prominent example, you can read about Shinichi Mochizuki's claimed proof of the so-called ABC Conjecture:

https://en.wikipedia.org/wiki/Abc_conjecture#Claimed_proofs


Replies

Reubendyesterday at 8:02 PM

For that particular example, it's now been proved that Mochizuki's proof is incomplete: https://zeli.app/en/story/48963019

I guess whether he will eventually fix those gaps and resolve the issues remains to be seen.