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