Hacker News Reader

singularity2001

they definitely do get answers. maybe the path is incomprehensible to you, but the yes or no answer is definitely there: that's what the formal provers are there for. In the worst case you have an Oracle which just answers your question with yes or no but in truth you get many more details if you want to look

View on HN

Is it a correct answer, though? Even with a Lean proof, someone has to be verify that it proved the right theorem.

Checking that the theorem is what we really want to prove is much much less work than going through the whole proof though.

Oh, absolutely. Just saying there’s something for mathematicians to do before publishing results.

Reply on news.ycombinator.com