logoalt Hacker News

gowldtoday at 12:13 AM1 replyview on HN

The "proof" is merely an appeal (unreadable program) submitted to a different oracle (Lean).


Replies

unified101today at 3:19 AM

What do u think lean is? That's like saying a program that works, is inscrutable because it appeals to the oracle of "code test cases" to prove itself correct.

You're either being intentionally obtuse, or unintentionally ignorant.

show 1 reply