| ▲ | monktastic1 an hour ago | |
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). | ||
| ▲ | gowld an hour ago | parent [-] | |
The "proof" is merely an appeal (unreadable program) submitted to a different oracle (Lean). | ||