arXiv cs.AI· Fedor Part, Valery Isaev, Sergey Sinchuk·· 11 小时前AI 评分20
JetBrains Research 的定理证明器 Arend 解析
Theorem prover Arend
AI 导读
JetBrains Research 开发的定理证明器 Arend 基于带立方体语法的同伦类型论变体，比完全计算的立方体类型论更贴近 MLTT，同时保留实用计算性质。其类与记录系统支持包容性子类型、部分实现和匿名扩展，IntelliJ Arend 插件可将 IntelliJ IDEA 变为完整 IDE，主库 arend-lib 涵盖构造代数、拓扑与合成同伦论形式化。
正文 · AI 翻译
摘要：本文阐述了 JetBrains Research 开发的定理证明器 Arend。Arend 语言的设计旨在促进在单价基础框架内对数学进行形式化，并侧重于构造性数学。它基于一种具有立方体语法的同伦类型论变体，该变体与 Martin-Löf 类型论（MLTT）更为接近，而非完全计算性的立方体类型论，同时仍保留了后者在实践中一些有用的计算性质。Arend 语言最显著的特性之一是其强大的类和记录系统，支持包含性子类型、部分实现和匿名扩展，这为构建定义层次结构提供了极大的灵活性。IntelliJ Arend 插件将 IntelliJ IDEA 转变为 Arend 语言的全功能集成开发环境（IDE），从而简化了 Arend 中的形式化工作。主要的 Arend 库 arend-lib 包含构造性代数、拓扑学和合成同伦论方面的形式化。
| 主题： | 计算机科学中的逻辑（cs.LO）；人工智能（cs.AI） |
| 引用为： | arXiv:2610.27264 [cs.LO] |
| （或 arXiv:2610.27264v1 [cs.LO] 用于此版本） | |
| https://doi.org/10.48550/arXiv.2610.27264 由 DataCite 颁发的 arXiv DOI（待注册） |
提交历史
来自：Fedor Part [查看电子邮件]
[v1]
2026年10月19日星期一 20:36:59 UTC（77 KB）
来源：arXiv cs.AI · arxiv.org