JetBrains Research 定理证明器 Arend 论文详解

JetBrains Research 撰文介绍其定理证明器 Arend，该语言基于带 cubical 语法的同伦类型论变体，比完全可计算的 cubical 类型论更贴近 Martin-Löf 类型论（MLTT），面向单价基础下的数学形式化，侧重构造性数学。