100 theorems in Lean
a year ago
- #formal-verification
- #mathematics
- #theorem-proving
- Freek Wiedijk 维护了一个追踪定理证明器在形式化数学中100条经典定理进展的清单
- 目前有81条定理已在Lean中完成形式化，另有0条定理仅完成了命题的形式化陈述
- 该清单包含著名定理，如2的平方根的无理性、代数基本定理和毕达哥拉斯定理
- 每条定理都标注了一位或多位贡献者，例如Chris Hughes、Joseph Myers和Jeremy Avigad
- 该清单作为比较不同定理证明器的基准，并通过GitHub拉取请求鼓励社区贡献