News for hackers. Stuff that matters.

A comment on The Mathocalypse. Parent comment

Re:The Mathocalypse by cgh on Thursday October 08, 2026 @10:10AM (#50006027)
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.
[ Parent | on HN ]
Re:The Mathocalypse by pasquinelli on Thursday October 08, 2026 @11:43AM (#50007223)
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?

[ Parent | on HN ]