概念
定理证明器
形式化验证工具链的核心组件，要求用户提供逐步的证明脚本，由内核机械检查每一步推理是否合法，代表工具有Coq、Isabelle、Lean。
时间轴 (近 90 天)
10月27日
类型系统、证明系统与定理证明器之间的关系可理解为强度与成本的连续谱：类型系统自动化程度最高、代价最低；定理证明器表达力最强但门槛最高；依赖类型、精化类型和契约式设计介于两者之间。
待验证50%
10月23日
LLM 生成的验证工件需要交给定理证明器或 SMT 求解器检查，形成“生成-检查”闭环，这是 LLM 辅助验证能被信任的机制基础。
待验证50%
10月18日
定理证明器的内核是负责检查证明正确性的最小可信组件。
待验证50%