知识/定理
液体张量实验（2018–20）：朔尔策与形式化社区用 Lean 证明助手完全形式化凝聚数学核心定理。
公式
凝聚态数学中「固体」代数 $\underline{R}$；完全形式化证明在 Lean mathlib 中核验。
证明思路
把前沿抽象数学翻译为 Lean 证明脚本，社区协作完成「不可能」的形式化。
应用/例子
Lean mathlib 的形式化标准；「前沿数学可被机器核验」的示范。
意义/影响
数学家与形式化社区的标志性合作——「抽象程度最高的数学也能被机器验证」。
DOXA · 数学编年史 · 知识详情
2018–20 ｜ 朔尔策/社区 ｜ 逻辑 ｜ 突破
液体张量实验（2018–20）：朔尔策与形式化社区用 Lean 证明助手完全形式化凝聚数学核心定理。
凝聚态数学中「固体」代数 $\underline{R}$；完全形式化证明在 Lean mathlib 中核验。
把前沿抽象数学翻译为 Lean 证明脚本，社区协作完成「不可能」的形式化。
Lean mathlib 的形式化标准；「前沿数学可被机器核验」的示范。
数学家与形式化社区的标志性合作——「抽象程度最高的数学也能被机器验证」。