Why is it all in the kernel?

A soundness bug in the Lean proof assistant kernel allowed a false 'proof' of the Collatz conjecture's negation to pass verification, even fooling the independent Nanoda checker. The author uses this incident to argue against the design philosophy of putting complex features like nested inductive types and recursive functions directly into proof kernels. Drawing on decades of experience with Isabelle and HOL systems, the author advocates for the LCF-style 'honest toil' approach: deriving advanced constructs (inductive definitions, recursive functions, pattern matching) from minimal primitive axioms outside the kernel, rather than 'postulating' them inside it. This keeps the trusted kernel small and reduces the attack surface for soundness bugs. Systems like HOL Light and HOL4 are cited as exemplars of this safer approach.

Nguồn: https://lawrencecpaulson.github.io/2026/07/30/Collatz.html. 8sync News chỉ tóm tắt và dẫn link; bản quyền nội dung thuộc tác giả và nguồn gốc.