Correctness of the kernel and consistency of the theory implemented in it are di... | Hacker News

Hacker Newsnew | past | comments | ask | show | jobs | submit

unexpectedtrap 11 months ago | parent | context | favorite | on: Project to formalise a proof of Fermat’s Last Theo...

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.

codebje 11 months ago [–]

Interesting - what is correctness of the kernel here? That it faithfully implements the model?

Consider applying for YC's Fall 2026 batch! Applications are open till July 27.
Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact