logoalt Hacker News

mathisfun123 • yesterday at 10:46 PM • 2 replies • view on HN

With so many results in so many different areas no way they even remotely spot checked well enough.

Prediction: one of these is wrong and this (publicity stunt) will backfire.

Edit: don't tell me about lean. For lean to function as a proof certificate you need to represent the theorem correctly. Again: good luck doing that across such a broad swath of problems.


Replies

bravoetch • yesterday at 10:49 PM

What does a backfire look like? It's ok to be wrong in the science/math world.

➕ show 1 reply
jojva • yesterday at 11:08 PM

You have not read their readme:

> Some of the unformalized results could have issues. We will endeavor to fix any such issues quickly. We are also exploring community-hosted repositories for these materials.

➕ show 1 reply