用证明论分析 AI 生成的数学证明：机器证明压缩率仅 31%
Studying proof data with proof theory: the case of AI-generated mathematics
OpenAI 那些形式化证明被拿来用证明论量化分析，AI 写的证明比人类长得多，31% 对 73% 这组数字很直观。
一篇 arXiv 论文提出用证明论方法分析大量形式化验证的数学证明，将证明项大小、冗余步数等指标转化为对证明本身的测量。对照 mathlib 参考库和各证明自身的 cut-free 形式，作者测量机器生成数学与人类数学的差异。结果显示 AI 写的证明实现的逻辑压缩率仅为 31%，mathlib 中人类证明为 73%；在不调用自动化的证明上，AI 为 55%，人类为 86%。这与自动定理证明工具开发者关于 AI 证明偏长的报告一致。
Studying proof data with proof theory: the case of AI-generated mathematics
I present a method for analyzing large collections of formally verified mathematical proofs (e.g. OpenAI's) grounded in some historical and philosophical musings on mathematics in the age of AI. Many of the quantities involved, such as the size of a proof term or the number of redundant steps, are already computed by work on improving automated provers, where they serve as targets. My aim is to turn them into measurements of proofs themselves: compared against a reference library and against each proof's own cut-free form, checked against theorems they must obey, and controlled for how the proofs were compiled. With these instruments, I measure how (much) machine-generated mathematics diverges from human mathematics, and find that AI-written formal proofs realize far less of the logical compression available to them than human mathematicians do (31% against 73% in mathlib, and 55% against 86% on proofs that call no automation). These figures are broadly in line with reports from those who build provers and proof-improvement tools that AI-written proofs are often longer than they need to be.
