isabelle

一篇实操性很强的博客文章，通过在 Lean、Isabelle/HOL、HOL4 和 Agda 中分别形式化欧几里得证明素数无穷性的论证，对这四个定理证明器进行了比较，并给出了关于易用性、交互性和使用体验的带有个人主见的排名。

Lawrence Paulson 讨论了因 Lean 内核中的一个 bug 导致的 Collatz 猜想的虚假反驳，并对证明对象和证明助手的可靠性进行了思考。

Galois 宣布，SAW 现在支持从 Cryptol 规范生成 Isabelle 理论，将 Cryptol 和 SAW 的易用性与 Isabelle 等交互式定理证明器的表达能力相结合，从而实现对加密协议的半自动化验证。