arXiv cs.AI· Fedor Part, Valery Isaev, Sergey Sinchuk·· 12 小时前AI 评分20
JetBrains Research 的定理证明器 Arend 解析
Theorem prover Arend
AI 导读
JetBrains Research 开发的定理证明器 Arend 基于带立方体语法的同伦类型论变体，比完全计算的立方体类型论更贴近 MLTT，同时保留实用计算性质。其类与记录系统支持包容性子类型、部分实现和匿名扩展，IntelliJ Arend 插件可将 IntelliJ IDEA 变为完整 IDE，主库 arend-lib 涵盖构造代数、拓扑与合成同伦论形式化。
正文 · 原文
Abstract:This paper is an exposition of the theorem prover Arend developed at JetBrains Research. Arend language has been designed to facilitate the formalization of mathematics within the framework of univalent foundations and with the focus on constructive mathematics. It is based on a variant of homotopy type theory with cubical syntax that is more closely aligned with Martin-Löf Type Theory (MLTT) than fully computational cubical type theories, while still retaining some of their computational properties useful in practice. Among the most notable features of the Arend language is its powerful system of classes and records supporting subsumptive subtyping, partial implementations and anonymous extensions, which provides extensive flexibility for constructing hierarchies of definitions. Formalization in Arend is streamlined by the IntelliJ Arend plugin, which transforms IntelliJ IDEA into a full-fledged integrated development environment (IDE) for the Arend language. The main Arend library arend-lib includes formalizations in constructive algebra, topology and synthetic homotopy theory.
| Subjects: | Logic in Computer Science (cs.LO); Artificial Intelligence (cs.AI) |
| Cite as: | arXiv:2610.27264 [cs.LO] |
| (or arXiv:2610.27264v1 [cs.LO] for this version) | |
| https://doi.org/10.48550/arXiv.2610.27264 arXiv-issued DOI via DataCite (pending registration) |
Submission history
From: Fedor Part [view email]
[v1]
Mon, 19 Oct 2026 20:36:59 UTC (77 KB)
来源：arXiv cs.AI · arxiv.org