一篇新论文通过将 Mathlib（Lean 4 中最大的形式化数学库）视为一个网络来进行分析。研究人员发现，该库基于文件夹和命名约定的组织结构，与其定理之间的实际数学依赖关系不符。研究还显示，很大一部分逻辑依赖关系跨越了命名边界，并且许多连接是由编译器隐式生成的，而不是由人类显式编写的。此外，网络分析表明，最常使用的元素是等词的自反性，而不是像中国剩余定理那样在数学上更深刻的定理。 AI
影响 为分析形式化数学库提供了一个框架，可能为未来 AI 生成的证明系统提供信息。
排序理由 分析大型形式化数学库的学术论文。
在 Mastodon — fosstodon.org 阅读 →
AI 生成摘要 · Google Gemini · 来自 2 个来源。 我们如何撰写摘要 →
"The Network Structure of Mathlib" Post by Simone Severini on LinkedIn: 2/2 ===== ... We read Mathlib as a transitional object, i.e., mathematics in the middle of moving from paper to machine, carrying traces of both worlds. These metrics, and the methods used to extract them, ma…
"The Network Structure of Mathlib" Post by Simone Severini on LinkedIn: 1/2 ===== New paper with Xinze Li (lead), Nanyun (Violet) Peng, and Patrick Shafto. Mathlib is the largest library of formalized mathematics in Lean 4. Every theorem is checked by a computer, and every proof …