Freek Wiedijk 一直在根据 100 个著名定理列表中的形式化定理数量对Proof assistant进行排名。截至 2023 年 9 月，只有五个系统正式证明了超过 70% 的定理，即 Isabelle、HOL Light、Coq、Lean 和 Metamath
--
FROM 101.24.89.*