JetBrains Research 开发的定理证明器 Arend 论文

JetBrains Research 发布定理证明器 Arend 的论文，该工具旨在支持同伦类型理论和构造主义数学的形式化。 Arend 语言基于同伦类型理论立方体语法变体，支持类、记录及子型系统。 IntelliJ Arend 插件将其集成至 IntelliJ IDEA，arend-lib 库包含构造代数和拓扑学的形式化内容。