groupoid/groupoid.space

# Groupoid Infinity 形式数学研究所的 Groupoid Infinity 实验室致力于形式化数学工具的研究与开发， 为数学证明与分析创建编程语言，以及通过现代计算方法进行定理验证。 ## 关于实验室 Groupoid Infinity 计算数学实验室负责为数学家开发和研究编程语言。 ## 工作流程 实验室的工作基于核心产出——定理验证方法论 AXIO/1 以及 AXIOSIS 语言系统。 该系统支持以多种方式对任意数学定理进行机械化处理： * 直接将理论原语嵌入验证器（用于最高效的计算）。 * 在其他理论中计算原语（用于研究原语基中的可推导性）。 ## 使命 为所有数学提供强大的计算语义。 ## 实验室工作原则 * 显式类型化 —— 明确定义类型，以提升速度、可靠性与透明度。 * 最小化核心 —— 研究紧凑高效的基础构造。 * 支持强属性 —— 保证数学正确性与严格不变式。 * 聚焦类型检查速度 —— 优化类型检查流程以增强实用性。 * 教学性与简洁性 —— 打造易于理解的工具，便于教学与研究。 * 模块化与可组合性 —— 开发可扩展、可组合的系统。 * 形式化验证 —— 证明程序与数学构造的正确性。 * 最小化依赖 —— 最好完全没有依赖。 * 抽象的通用性 —— 为广泛的数学任务创建灵活的工具。 ## 科学方向 * 微分几何 * 代数拓扑 * 超几何 * 稳定同伦色彩理论 * 单纯几何 * 类型论视角下的 K 理论 ## 已开发的编程语言 * Laurnt Schwartz —— 用于泛函分析的类型论。 * Ernst Zermelo —— 包含排中律的 ZFC 类型论。 * Paul Cohen —— 用于包含大基数和力迫的基数系统的类型论。 * Henk Barendregt —— 用于纯依赖 Lambda 演算的类型论。 * Per Martin-Löf —— 用于纤维化方法与归纳类型的类型论。 * Anders Mörtberg —— 用于立方 CCHM/CHM/HTS 变体的类型论。 * Dan Kan —— 单纯同伦类型论（支持 Kan、Rezk、Segal 模式）。 * Fabien Morel —— 用于 A¹ 同伦论的类型论。 * Jack Morava —— 用于色彩同伦论和 K 理论的类型论。 * Urs Schreiber —— 用于等变超几何的类型论。 ## 项目状态 该系统实现了合成数学与经典数学的综合。其类型涵盖： * 单纯 ∞-范畴 * 稳定谱 * 模态 * 实数 * ZFC * 大基数 * 力迫 截至 2025 年，所有已知的数学领域均已集成至该系统中，可在统一的计算范式下进行处理。

标签：AXIO/1, AXIOSIS, Groupoid Infinity, 代码分析, 凭证管理, 函数式编程, 定理证明, 定理验证器, 形式化数学, 数学软件, 数理逻辑, 程序验证, 符号计算, 类型理论, 编程语言设计, 计算机科学, 证明助手, 语义学