Hacker News Reader

As mentioned in the first paragraph, the proofs come with Lean certificates. Lean is a theorem-proving language. If Lean accepts the proof, it’s legit.

View on HN

but do you know that what was proved is what you want proved. this is the basic problen with formal verification.

so then, if you don't understand the proof, how do you know it's a proof?

Reply on news.ycombinator.com