Re:The Mathocalypse
by pasquinelli on Thursday October 08, 2026 @08:56AM
(#50005278)
i'm confused how it is that no one understands the proofs but still assume they are proofs.
[ Parent
| on HN ]
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.
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?