Show HN: Lean4 证明 SSOT 需要定义时钩子和自省
发布: (2026年1月8日 GMT+8 13:15)
1 min read
原文: Hacker News
Source: Hacker News
Overview
我在 Lean 4 中形式化了单一真相来源（SSOT）原则（约 2.1k LOC，零 sorry），并证明了两个核心结果：
- 结构化的 SSOT 仅在语言提供定义时钩子和运行时自省时才可实现。
- 宏/代码生成（定义前）和反射（定义后）是实现此功能的机制。