On: The Mathocalypse

[pasquinelli]

i'm confused how it is that no one understands the proofs but still assume they are proofs.

[pred_ → pasquinelli]

They already had to withdraw three of the manuscripts and correct several others. Who knows how much broken stuff there's in there; unfortunately they were too lazy to check themselves.

[cgh → pasquinelli]

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.

[pasquinelli → cgh]

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?