本文介绍了由 JetBrains Research 开发的定理证明器 Arend（arXiv:2610.27264v2）。Arend 语言旨在在同伦基础（univalent foundations）框架下，侧重构造性数学地形式化数学。它基于一种带有立方体语法的同伦类型理论变体，与 Martin‑Löf 类型理论（MLTT）更为接近，同时保留了部分计算性特征，便于实际使用。
Arend 的核心特性之一是强大的类（class）和记录（record）系统，支持下溯子类型（subsumptive subtyping）、部分实现和匿名扩展，从而在构建定义层次结构时提供了极大的灵活性。
为了简化形式化工作，IntelliJ Arend 插件将 IntelliJ IDEA 打造成完整的 Arend 开发环境（IDE），提供语法高亮、自动补全和交互式检查等功能。
Arend 的标准库 arend‑lib 包含了构造性代数、拓扑学以及合成同伦理论的形式化实例，展示了语言在实际数学研究中的应用。
点评