logoalt Hacker News

gowldyesterday at 11:10 PM1 replyview on HN

But the "computer" is magic, to you.

I could prove anything by claiming I completed a trivial-to-explain exhaustive search. The only support or refutation would be someone doing their own search. It's a very weak foundation.

We already had the ABC conjecture crisis: A theorem with a human-written proof so complex that no one besides the author can understand it. Some people claim to have refuted it. Most mathematicians are unqualified to decide.


Replies

odyssey7today at 1:00 AM

If you prove that the theorem prover’s true and false determinations are correct—in the cases in which it can make them—then Bob’s your uncle.