Live data from Hacker News

Many "serious" mathematicians are aghast

twitter.com

31–32 of 32 posts

Re: Many "serious" mathematicians are aghast

#31

If these proofs were output by the AI in a format readable by a proof verification system, the verification step of publishing vanishes. Then it's only valuable to check if the stated intention actually matches the proof and isn't something completely different.

I don't know why your comment is downvoted, because it makes much sense. That's assuming the proof is not founded in assumptions, and the proof checker doesn't have bugs.

https://en.wikipedia.org/wiki/Lean_(proof_assistant)

Not sure about "bugs" in that area, but there is a lot of work going on by mathematicians in formalizing and checking ever more complex proofs using proof assistants.

These systems have been tested on very complex proofs already, but well... I'm not a mathematician, just a software engineer who accepted his new role in this "new thinking order".

Re: Many "serious" mathematicians are aghast

#32
post #18

This is Lemire so take it with a big grain of salt. Some notable mathematicians including Fields medalists are not 'aghast'.

Since when did Lemire need to be taken with a grain of salt?

Since about 2020. He's become strange and conspiratorial around COVID-19, and around LLMs more recently.
Post reply on HN