alt Hacker NewsBut this oracle doesn't just say true / false. It also gives a proof. That makes it much less exciting (not to mention beneficial for your career) to find another one (or even worse, the same one).
But this oracle doesn't just say true / false. It also gives a proof. That makes it much less exciting (not to mention beneficial for your career) to find another one (or even worse, the same one).
The "proof" is merely an appeal (unreadable program) submitted to a different oracle (Lean).