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 10 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 10 months ago [–]

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

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact