Tactician 的大规模形式知识网

Tactician's Web 是一个平台，提供了一个由强互联、机器检查的形式数学知识构成的大型网络，并便捷地打包用于机器学习、分析和证明工程。该平台构建于 Coq 证明助手之上，导出了一个包含各种形式理论的数据集，呈现为定义、定理、证明项、策略和证明状态的网络。理论被编码为语义图（如下所示）和人类可读文本，各自具有独特的优缺点。证明智能体可以通过同样丰富的数据表示与 Coq 交互，并可以在一组定理上自动进行基准测试。与 Coq 的紧密集成提供了独特的可能性，即让证明工程师将智能体作为实用工具使用。