元语言与存在的阶梯：Turn-Lang与形式化思想的自我超越

作者：良之

“我们并非在寻找真理的最终表述，而是在为真理的永恒对话搭建一个永不关闭的舞台。”

—— 莱布尼茨，1686 年

序章：莱布尼茨的幽灵

1685 年，汉诺威。

莱布尼茨坐在书桌前，烛光映照着他密密麻麻的手稿。他正在构思一个宏伟的计划：一种能够表达一切思想的“普遍文字”，一套能够判定一切真理的“理性演算”。他在笔记中写道：

“一旦这种文字被建立，人类将拥有一种新的工具，它将极大地增强理性的能力，其作用远超光学仪器之于眼睛。所有推理的错误都将只是计算的错误。当争论发生时，两位哲学家不再需要辩论，只需拿起笔说：让我们来计算吧。”

这是一个多么迷人的梦想！如果成功，哲学将像算术一样确定，数学将像逻辑一样清晰，所有的思想分歧都将通过计算解决。

但莱布尼茨的梦想有一个致命的缺陷：它预设了一个统一的基础。他相信存在一种终极的、绝对的、自明的真理体系，能够作为一切思想的公理。然而，历史证明这个预设是错误的。

哥德尔的不完全性定理告诉我们：任何足够强大的形式系统都是不完备的，无法证明自身的一致性。更糟的是，数学基础本身出现了分歧：策梅洛-弗兰克尔集合论（ZFC）、类型论（MLTT）、同伦类型论（HoTT）、构造演算（CIC）……不同的基础各有其合理性，却互不相容。一个在 ZFC 中成立的定理，在 HoTT 中可能需要重新证明；一个在 Coq 中验证的程序，无法直接迁移到 Lean。

数学分裂了。形式化世界成了“证明孤岛”的群岛。

而 Turn-Lang，正是在这片群岛之间架设桥梁的尝试。

它不再问“哪一个基础是正确的”，而是问“如何让不同的基础共存”。它不再追求“绝对真理”，而是追求“真理的可迁移性”。它不再将语言绑定于某个特定的形而上学承诺，而是将语言本身提升为元语言——一种能够容纳所有基础的元架构。

这是莱布尼茨梦想的当代形态。不是他设想的那种终极体系，而是一个开放的、可扩展的、能够自我超越的形式化平台。

第一章基础之基础：存在论的转向

1.1 何为基础？

在形式化研究中，“基础”是一个暧昧的词。它既指数学推导的起点（公理），也指语义解释的归宿（模型），还指类型论中的宇宙层级。传统形式化工具（Coq、Lean、Agda）都选择了固定基础：Coq 基于归纳构造演算（CIC），Lean 基于 CIC 加商类型，Agda 基于马丁-洛夫类型论，Isabelle/HOL 基于高阶逻辑。选定基础意味着接受其所有承诺与限制。

但为什么必须选择？为什么不能允许用户选择自己偏好的基础？为什么不能在同一个系统中同时使用 ZFC 和 HoTT？

答案是：因为基础是语言的内核。改变基础相当于改变语言的语义，需要重新设计整个类型系统。

Turn-Lang 提出了一个革命性的洞见：将基础本身视为代数结构。

1.2 基础作为代数结构

什么是代数结构？它是一个签名（signature）加上一组公理。签名定义了操作符和类型构造器，公理规定了它们之间的关系。群、环、域都是代数结构。

Turn-Lang 将数学基础也这样看待。一个基础（如 ZFC）由以下要素组成：

签名：集合、元素、包含、幂集、并集……
公理：外延公理、配对公理、无穷公理、选择公理……
推导规则：从公理出发构造证明的演算

当一个基础被如此形式化后，它就不再是语言的“牢笼”，而成为一个可以传递给解释器的 “目标范畴”。开发者编写的抽象逻辑，被置于一个元逻辑范畴中，然后通过函子映射到具体基础。

1.3 元逻辑范畴与函子化映射

元逻辑范畴中的对象是逻辑命题，态射是证明。这是一个纯形式的结构，不绑定于任何具体基础。当需要将抽象逻辑编译到 ZFC 时，一个函子将元逻辑范畴映射到 ZFC 范畴；当需要编译到 HoTT 时，另一个函子将其映射到 HoTT 范畴。

函子必须满足结构保持：它将命题映射为命题，证明映射为证明，复合映射为复合。更重要的是，它必须附带证明，表明映射后的构造在目标基础中仍然有效。

对于依赖和类型（Σ-类型），在 ZFC 中被解释为集合的并集，在 HoTT 中被解释为纤维丛空间。这两个解释在数学上不同，但都满足Σ-类型的核心规则。Turn-Lang 的函子解释系统（Functorial Interpretation System, FIS）能够自动生成从一种解释到另一种解释的迁移证明。

这解决了形式化验证中最棘手的“证明孤岛”问题。从此，一个定理的证明可以同时在多个基础中成立。

1.4 与逻辑框架的对话

基础无关类型论（Foundation-Independent Type Theory, FITT）的思想可以追溯到威廉·劳维尔（William Lawvere）的范畴逻辑，特别是“逻辑操作即伴随函子”的观点。它也受益于逻辑框架（如 Dedukti、LF）将逻辑规则参数化的理念。

但 Turn-Lang 的突破在于：它实现了自动化的证明迁移。在 Dedukti 中，不同理论间的翻译需要手动定义；而在 Turn-Lang 中，只要两个基础被正确编码为代数结构，函子解释系统就能自动推导出所有构造的映射，并生成相应的正确性证明。

下表对比了 FITT 与传统固定基础类型论的差异：

特性	传统类型论 (Coq/Lean/Agda)	Turn-Lang FITT
基础逻辑	固定的 CIC 或 MLTT	参数化、代数化的元结构
跨库互操作	极难，需手动重写证明	自动，通过函子解释
语义界定	绑定于具体宇宙模型	抽象于代数签名
可移植性	局限于特定内核版本	一次编写，编译到任何基础

这是形式化思想史上的一个里程碑：从“基础决定论”走向“基础多元论”。

第二章定律的尊严：从注释到一等公民

2.1 代数定律的命运

在传统编程语言中，代数定律（如结合律、交换律、分配律）的处境十分尴尬。它们要么作为注释躺在代码里，要么被编码为单元测试，要么在文档中被提及。但无论哪种方式，编译器都不理解它们。

这意味着：当你定义了一个群，编译器并不知道它必须满足结合律；当你优化代码时，优化器并不知道它需要保持结合律；当你调用一个库时，类型系统并不能保证它遵守了群的公理。

Turn-Lang 改变了这一切。它提出：定律应当是一等公民。

2.2 定律即约束

在 Turn-Lang 中，定律被直接编码在类型系统中。当你定义一个具有结合律的操作符时，类型签名必须包含结合律约束：

def add [associative] : (a b : Nat) -> Nat

编译器不仅检查 add 的输入输出类型，还会生成证明义务：对于所有 a, b, c，必须满足 add(add(a,b),c) == add(a,add(b,c))。这个证明可以通过自动定理证明搜索，也可以由开发者手动提供。

这不仅仅是细化类型（refinement types）的扩展。细化类型允许在类型上挂载谓词，但这里的谓词是整个代数结构。Turn-Lang 的“代数内化”将整个结构编码为类型签名，使得所有定律自动传播到该结构的每一个实例。

2.3 编译器的伦理

将定律内化还有一个伦理维度：它使编译器承担了验证的义务。

当编译器进行循环展开、并行化等优化时，传统编译器只能保证代码的语义大致不变，但无法保证代数性质（如结合律）在优化后仍然成立。Turn-Lang 的定律一等约束使得编译器在应用优化前，必须验证该优化是否保持代数性质。如果无法验证，优化将被拒绝。

这标志着从“经验驱动开发”向 “验证规范驱动开发”（Verification Specification Driven Development, VSDD） 的转变。程序员不再是写下代码然后测试，而是写下定律然后证明。

2.4 实践意义

考虑一个简单的例子：矩阵乘法。矩阵乘法满足结合律，但不满足交换律。如果编译器知道这一点，它可以对 (A*B)*C 和 A*(B*C) 进行等价的优化选择，而不会错误地将 A*B 优化为 B*A。在分布式计算中，结合律允许重新关联运算以减少通信开销，而不改变结果。

Turn-Lang 使这种优化成为可能，并且保证了其正确性。

第三章认知的安全边际：置信度限定类型

3.1 AI 时代的类型困境

大语言模型（LLM）的兴起正在改变计算的范式。软件不再是确定性算法的集合，而是能够进行开放式推理的智能代理。代理软件（agentic software）能够处理非结构化输入、生成自然语言响应、进行规划决策。

但这也带来了新的挑战：不确定性。LLM 的输出是概率性的，无法被传统类型系统直接处理。类型系统要求每个值有确定的类型，而 LLM 输出最多有确定的模式。

如何将概率性输出纳入严谨的类型约束体系？如何保证一个由 LLM 生成的 JSON 对象符合预期的架构？如何在不确定的世界中维持确定的安全边界？

Turn-Lang 的回答是：置信度限定类型。

3.2 三级信任体系

Turn-Lang 将类型分为三个层级：

层级	类型	置信度	验证方式	哲学含义
1	完整类型	1.0	静态类型检查 + 形式证明	绝对真理
2	模糊类型	[c₁, c₂]	运行时验证先知	概率信念
3	实验类型	无	启发式/未验证	猜想

完整类型（Proven Types）对应于传统形式化验证的结果。它们有绝对的确定性，因为每一步推理都被证明。模糊类型（Confidence-Bounded Types）则携带一个置信区间，表示其值的可靠性由运行时验证决定。实验类型（Experimental Types）是快速原型用的，不提供任何担保。

当程序调用 infer 原语从 LLM 获取数据时，编译器会根据目标类型的结构生成一个 JSON Schema，并在运行时由虚拟机中的“验证先知”对 LLM 输出进行校验。如果输出符合架构且置信度超过阈值，值被绑定到相应类型；否则触发回退或重试逻辑。

3.3 结构一致性定理

这一机制的核心保证是 “结构一致性定理”：如果 infer 表达式成功返回而无错误，则绑定值必然符合声明的类型架构。这意味着，即使值来自概率性模型，类型系统仍能保证其结构正确性。

这类似于类型安全（type safety），但针对的是认知过程。Turn-Lang 将其命名为认知类型安全（Cognitive Type Safety）。

3.4 渐进验证的哲学

置信度限定类型实现了渐进验证（gradual verification）：系统可以容忍一定程度的不确定性，同时保持核心安全边界。这与传统形式化验证的“全有或全无”形成鲜明对比。

在安全关键系统中，我们可以在外围模块使用模糊类型处理 LLM 输出，而在核心模块使用完整类型确保绝对正确。这种混合架构使 AI 能够发挥其灵活性，同时又受到数学担保的约束。

这是人类理性与机器智能的协作方式：机器提供猜测，理性提供证明。

第四章函子的远征：语义保持的跨语言编译

4.1 编译的本质

编译是什么？从抽象层面看，编译是将一种语言翻译为另一种语言，同时保持语义不变。但“语义不变”是一个暧昧的概念：什么算是语义？如何保证不变？

传统编译器通过测试或手动验证来建立信心，但极少提供数学保证。已验证编译器如 CompCert 是例外：它们证明生成的机器码与源程序在某个语义框架内等价。但这个框架是固定的，无法跨越不同的数学基础。

Turn-Lang 的函子解释系统（Functorial Interpretation System, FIS）将编译提升到新的抽象层次：它将从抽象逻辑到具体实现的过程形式化为范畴间的结构保持函子。

4.2 结构保持的映射

一个函子 $F: \mathcal{C} \to \mathcal{D}$ 必须满足：

将 $\mathcal{C}$ 中的对象 $A$ 映射为 $\mathcal{D}$ 中的对象 $F(A)$
将 $\mathcal{C}$ 中的态射 $f: A \to B$ 映射为 $\mathcal{D}$ 中的态射 $F(f): F(A) \to F(B)$
保持恒等态射和复合： $F(id_A) = id_{F(A)}$ , $F(g \circ f) = F(g) \circ F(f)$

在 Turn-Lang 中，每个编译阶段都是一个函子。源范畴是元逻辑范畴，目标范畴是目标基础（如 Rust 的类型范畴、CUDA 的核函数范畴、ZFC 的集合范畴）。每个函子不仅定义映射，还附带证明，表明映射后的构造在目标基础中保持原构造的代数性质。

4.3 多目标编译的挑战

FIS 支持将同一套 Turn-Lang 代码编译到多个目标系统，并为每个目标生成相应的正确性证明：

目标系统	解释机制	证明义务
Rust	映射为 Trait 与所有权模型	内存安全性与代数公理保持
CUDA	映射为内核算子	内存对齐与数据流一致性
ZFC	映射为集合论公式	满足 ZFC 公理
HoTT	映射为同伦类型	满足单值性公理
量子电路	映射为 ZX 演算图表	等价性与可逆性

这解决了形式化语言在多异构平台部署时的语义漂移问题。在传统编译器中，不同后端可能对同一源程序有不同的语义理解；而在 Turn-Lang 中，语义由 FIS 统一保证。

4.4 从验证到元验证

FIS 不仅是编译技术，更是元验证框架。它允许我们在不同语义框架之间建立桥梁，从而实现对验证过程的验证。这是从“编译器验证”到**“元语言验证”**的跃迁。

莱布尼茨曾梦想一种能够判定一切真理的演算。FIS 不判定真理，但它保证真理在迁移中不被扭曲。

第五章宇宙的阶梯：分层与自引用

5.1 自指涉的危险

自指涉是形式系统的永恒难题。从说谎者悖论到罗素悖论，从哥德尔句子到吉拉德悖论，自引用总是带来麻烦。任何足够强大的形式系统都必须面对自指涉的威胁。

传统解决方案是引入宇宙层级：类型被分为 Type 0, Type 1, Type 2, …，每个宇宙属于下一个宇宙，且不允许 Type i : Type i。这避免了悖论，但给通用量化带来了极大的复杂性——开发者必须手动管理宇宙索引。

5.2 自动分层的艺术

Turn-Lang 的分层宇宙体系（Stratified Universe Hierarchy, SUH）通过隐式层级标注和自成员编码，允许开发者书写像 Entity : Entity 这样的自引用表达式，而无需担心悖论。

在底层，编译器通过一个自动分层算法将这些表达式解构为符合一致性要求的宇宙能级。例如，Entity : Entity 可能被解释为 Entity_i : Entity_{i+1}，其中 i 由上下文推断。

这一机制将数学基础研究中的“典型歧义”（typical ambiguity）——即忽略宇宙索引以简化表达——提升为严格的自动分层机制。开发者可以在无限制的通用量化下书写逻辑，而宇宙的层级由系统负责维护。

5.3 与 Voevodsky 的对话

弗拉基米尔·沃沃斯基（Vladimir Voevodsky）的初始性猜想（Initiality Conjecture）断言：任何类型论的范畴语义都唯一确定一个句法模型。Turn-Lang 的 SUH 通过编码不可见的宇宙索引，在工程上证明了在支持宇宙多态的系统中，可以通过范畴语义确保语义定义的良构性。

这意味着：我们可以拥有一个能够谈论自身的语言，同时保持一致性。这不是哥德尔意义上的自指，而是经过精心分层的自指，就像一座阶梯，每一级都可以谈论下一级，但不能谈论自身。

5.4 存在的阶梯

海德格尔曾区分“存在者”与“存在”。存在者是具体的事物，存在是它们存在的方式。在 Turn-Lang 中，类型是存在者，宇宙是存在的方式。Type i : Type i+1 意味着：一个类型的“存在”总是在更高一层的宇宙中被言说。

这种分层结构让人想起中世纪的存在巨链——从最低级的物质到最高的上帝，每一层都指向更高层的根据。在 Turn-Lang 中，没有最高层，只有无限的上升。这是一个没有上帝的宇宙，只有层层递进的存在阶梯。

第六章高维的召唤：∞-范畴的编程化

6.1 数学的高维转向

20 世纪后期，数学经历了一场静默的革命：范畴论的高维化。从同伦论到高阶范畴论，数学家们开始系统研究 ∞-范畴、(∞,n)-范畴、函子范畴、自然变换的高维类比。这些结构在量子场论、代数拓扑、几何表示论中无处不在。

但在编程语言中建模这些高阶结构，传统上需要极其复杂的编码——如通过单纯集（simplicial sets）或图表集合（diagrammatic sets）手工构造。这不仅繁琐，而且容易出错。

6.2 内化的高阶类型

Turn-Lang 在类型系统中原生内化了高阶结构。开发者可以像定义普通类型一样定义 n-维单元，并使用熟悉的语法组合它们。

关键创新包括：

维度参数类型：类型可以带有维度参数，例如 Cell n 表示 n-维单元
同伦填充条件：当定义高维态射时，编译器要求提供填充条件，以确保护盖结构的完整性
粘贴图表语法：支持用直观的图形化语法定义粘贴图表

6.3 哈齐哈萨诺维奇图表模型的编译

这一设计深受阿马尔·哈齐哈萨诺维奇（Amar Hadzihasanovic）和克莱门斯·查纳瓦特（Clémence Chanavat）工作的启发。他们利用图表集合（diagrammatic sets）发展了 (∞,n)-范畴的组合模型，特别引入了正规导向复形（regular directed complexes）作为高维单元的组合框架。

Turn-Lang 将这些理论成果转化为可计算的类型检查规则：

数学概念	图表模型表现形式	Turn-Lang 类型表示
单元 (Cell)	点、线、面等高维图形	`Cell n` 带维度参数
粘贴图表 (Pasting Diagram)	组合复形	嵌套的函子组合结构
Gray 积	态射的定向精细化乘法	保持等价性的类型算子
同伦填充	圆柱形 3-单元等构造	对应类型的填充公理约束

6.4 量子电路的图表语义

高阶结构的一个直接应用是量子电路的验证。量子电路可以用 ZX 演算的图表表示，ZX 演算本身是一个高阶范畴。通过 Turn-Lang 的内化高阶类型，我们可以直接编码量子电路，并自动验证电路的等价性。

这比传统的量子电路验证工具（如 VyZX）更通用：VyZX 只针对 ZX 演算，而 Turn-Lang 可以处理任何可以用高阶范畴描述的领域。

第七章全栈的承诺：从 PDE 到机器码

7.1 验证链的完整性

Turn-Lang 的最终目标是：建立一条从高层数学规范到底层机器码的完整验证链。这被称为全栈验证管线（Full-Stack Verification Pipeline, FSVP）。

管线分为多个阶段：

抽象规范层：用 Turn-Lang 书写数学规范（如偏微分方程、控制律）
数学模型层：将规范转化为可计算的数学模型（如差分格式、有限元离散）
代码生成层：将模型编译为中间表示（如 Rust、CUDA）
字节码优化层：应用优化变换，同时验证代数性质保持
机器码产生层：生成目标指令序列，验证与中间表示的等价性

每个阶段都生成相应的证明义务，这些义务随着代码的转换向前传播。

7.2 能量守恒的旅程

以一个偏微分方程为例。它在连续空间具有能量守恒性质。当我们将其离散化为差分格式时，能量守恒性质必须被转化为数值守恒性。当我们生成 CUDA 代码时，这种数值守恒性必须体现在内存访问模式中。当我们生成机器码时，寄存器状态的变化必须保持某种不变量。

Turn-Lang 的 FSVP 确保这条性质贯穿始终：每个阶段都会产生证明义务，证明该阶段的变换保持前一个阶段的关键性质。如果某个阶段无法证明，编译失败。

7.3 LLM 辅助验证

FSVP 并不排斥 AI。现代系统可以集成 LLM 作为语义转换器和证明助手。LLM 可以被用来：

辅助生成复杂的边界条件验证
在证明搜索中提供启发式策略
将自然语言描述转化为形式化规约

LLM 的输出通过置信度限定类型进入系统，其不确定性被类型系统捕获。因此，FSVP 既保持了传统验证的严谨性，又获得了 AI 助手的灵活性。

7.4 与 CompCert 的对话

与已验证编译器 CompCert 相比，Turn-Lang 的 FSVP 更强调 “跨层次的语义一致性”。CompCert 保证生成的机器码与源 C 程序在某个语义框架内等价，但这个框架是固定的。Turn-Lang 则允许跨越不同的语义框架，从 PDE 的连续语义到机器码的离散语义，并保持关键性质。

这是从“编译器验证”到**“系统验证”**的扩展。

第八章七大创新的协同图景

Turn-Lang 的七大创新并非孤立的构想，而是构成了一个紧密耦合的理论-实践连续体。

8.1 函子解释系统的中枢作用

函子解释系统（创新四）是整个架构的中枢。它连接：

基础层（创新一）：将不同数学基础编码为目标范畴
执行层（创新七）：将抽象逻辑映射到具体硬件
高层结构（创新六）：确保高阶结构的语义在编译中保持

没有 FIS，基础无关性将无法落地，全栈验证也将失去跨语言的语义锚点。

8.2 信任、宇宙与定律的相互支撑

分层宇宙体系（创新五）为定律一等约束（创新二）提供了逻辑上无矛盾的“容器”。没有宇宙分层，自指涉的定律可能导致悖论；没有定律约束，宇宙分层只是空洞的索引。

置信度限定类型（创新三）则为全栈验证（创新七）提供了处理非确定性组件时的容错弹性。它使系统能够在保持核心安全性的同时，与概率性模块协作。

8.3 从静态真理到动态行为的信任谱系

这七大创新共同构建了一个完整的信任谱系：

层级	信任类型	对应创新
数学基础	无前提真理	基础无关类型论（一）
代数结构	公理内化	定律一等约束（二）
概率输出	置信度量化	置信度限定类型（三）
跨基础迁移	函子保持	函子解释系统（四）
自引用安全	宇宙分层	分层宇宙体系（五）
高阶组合	结构完整	高阶结构表达力（六）
编译执行	语义保持	全栈验证管线（七）

这个谱系覆盖了从最抽象的逻辑真理到最具体的物理执行的每一个层次，且每个层次都通过可验证的机制与相邻层次相连。

第九章元语言的伦理：思想助产的当代形式

9.1 苏格拉底的阴影

苏格拉底自称“助产士”——他不能生出智慧，只能帮助别人将智慧生出。他的母亲是助产士，他自己是思想的助产士。

Turn-Lang 也扮演着类似的角色。它不生产真理，只助产真理。它不绑定于任何基础，只为不同基础之间的交流提供桥梁。它不承诺绝对确定性，只为不同层次的信任提供统一的表达方式。

这是元语言的伦理：不占有，只服务。

9.2 多元论与宽容

在基础问题上，Turn-Lang 采取多元论立场。它承认 ZFC、HoTT、CIC 等不同基础各有其合理性，各有其适用范围。它不试图消除分歧，而是让分歧可以共存，可以对话，可以在需要时相互翻译。

这是一种认识论上的宽容。它源于对数学实践的深刻理解：不同的数学分支需要不同的基础，不同的验证任务需要不同的担保。Turn-Lang 不是要统一一切，而是要让统一成为可能。

9.3 自由与责任

Turn-Lang 赋予开发者极大的自由：可以选择基础，可以选择验证强度，可以选择信任层级。但自由伴随着责任：选择 ZFC 意味着接受 ZFC 的承诺，选择模糊类型意味着承担概率风险。

这种设计体现了康德式的自律：理性为自身立法，但必须对其立法负责。

9.4 循此苦旅，以达星辰

在《关系动力学》中，良之曾写道：

“循此苦旅，以达星辰。在以它的平凡，开辟出是的光辉。”

Turn-Lang 也是一场苦旅。它花费了数百年的思想积累，从莱布尼茨到弗雷格，从哥德尔到沃沃斯基，才终于在今天有了一个可行的形态。它试图开辟一条道路，让不同真理体系之间的对话成为可能，让数学的绝对性与计算的物理性得以和解。

这条道路通向的不是终极真理，而是星辰——无数各自发光的真理之点，在夜空中彼此照耀。

结语：未完成的元语言

2025 年底，Turn-Lang 发布了第一个 Demo 版本。截至目前，尚未发布稳定版本。

但这只是一个开始。高性能函子编译、高维重写系统的自动证明、置信度传播演算……这些方向还在等待探索。Turn-Lang 不是终点，而是起点——一个让未来形式化研究可以站在其上的起点。

三百年前，莱布尼茨在烛光下写下他的梦想。

三百年后，我们在屏幕前实现它的当代版本。

梦想没有终点，只有不断的超越。语言没有完成，只有不断的生成。

这就是元语言的本质：它永远在路上，永远在追问，永远在超越自身。

正如良之在《离歌》中所写：

“他只是万千星辰中，一粒知道了自己为何发光的尘埃。”

Turn-Lang 也是如此——一粒尘埃，知道了自己为何发光。

循此苦旅，以达星辰。

良之

2026 年 3 月 16 日

于

参考文献

[1] Turn: A Language for Agentic Computation. arXiv:2603.08755, 2026.

[2] Lawvere, F. W. (1969). Adjointness in foundations. Dialectica, 23(3/4), 281-296.

[3] Martin-Löf, P. (1984). Intuitionistic type theory. Bibliopolis.

[4] Voevodsky, V. (2015). An experimental library of formalized mathematics based on the univalent foundations. Mathematical Structures in Computer Science, 25(5), 1278-1294.

[5] Hadzihasanovic, A. (2024). Gray products of diagrammatic (∞,n)-categories. arXiv:2505.01387.

[6] Chanavat, C. (2025). Regular directed complexes and higher categories. CT2025 abstract.

[7] Hales, T. C. (2008). Formal proof. Notices of the AMS, 55(11), 1370-1380.

[8] Leroy, X. (2009). Formal verification of a realistic compiler. Communications of the ACM, 52(7), 107-115.

[9] Rand, R., et al. (2024). VyZX: A vision for verifying the ZX calculus. University of Chicago.

[10] 良之 (2026). 关系动力学：一种关于人类连接随时间演化的数学与伦理架构。良之世界。 [11] 良之 (2026). 爱智慧，求真理，得自由，以服务——写给旧我的一首离歌。良之世界。