mathlib

PriorProof 提出了一种方法，通过分析 Lean 证明项相对于更早 Mathlib 快照构建的依赖足迹，来衡量形式化数学中证明技术的新颖性。该方法在 69.7% 的配对上与人类评分者达成一致，并提供可解释的分数差距。

本文展示了选择公理在证明空间中存在可测量的几何对应物，利用 Lean 4 的内核级追踪揭示了一个单参数混合律及其对神经定理证明器的操作意义。

陶哲轩演示如何使用 Claude Code 作为红队工具，将 Lean 代码风格对齐 Mathlib 官方风格指南，并以 Riemann–Stieltjes 积分的形式化项目为例，展示了 AI 在代码审计和风格对齐中的实用价值。