News for hackers. Stuff that matters.

A comment on Lean proof of Fermat's Last Theorem [pdf]. Parent comment

Re:Lean proof of Fermat's Last Theorem [pdf] by unexpectedtrap on Thursday August 21, 2025 @02:06AM (#44969540)
Correctness of the kernel and consistency of the theory implemented in it are different things. Gödel’s theorems prevent you from proving the latter, but not the former.
[ Parent | on HN ]
Re:Lean proof of Fermat's Last Theorem [pdf] by codebje on Thursday August 21, 2025 @08:54AM (#44972162)
Interesting - what is correctness of the kernel here? That it faithfully implements the model?
[ Parent | on HN ]