Re:Mathematics has changed. Let's act like it
by ericpruitt on Sunday November 01, 2026 @02:20PM
(#50328751)
Isn't it also possible that the written proofs themselves are incorrect, say, for example, by mis-specification of constraints? Let's say I publish what I claim is a proof that 2+2=4, but in the Lean specification, I proved 1+1=2.
[ Parent
| on HN ]
Re:Mathematics has changed. Let's act like it
by thevinter on Sunday November 01, 2026 @02:44PM
(#50329001)
To be pedantic, the proofs would be correct, they would just be proving the wrong thing.
To address what you actually meant: it's possible but specifications are way easier to verify.
Re:Mathematics has changed. Let's act like it
by oulipo on Sunday November 01, 2026 @02:50PM
(#50329075)
The main issue would rather that the formalization itself has a bug, eg. those proofs that you're trying to formalize are not "1 + 1 = 2" but theorems which take already multiple pages just to enunciate. And in these enunciations (that are made by humans) there can be errors.
In general, once the proof has been formalized, it's supposed to be the proof of the correct theorem (that's what the Lean proof-checker checks)