在这里，我展示了一篇最近数学论文的完整自动形式化（又一次！） Barańczuk, Stefan. "在有限域上定义 n-空间子集的方程数量减少。" 图卢兹科学学院年刊：数学，第 6 卷，第 33 期，第 1 号（2024）：177–182。 我在这个项目上花了几天时间。首先，我通过 @HarmonicMath 运行了亚里士多德，经过大约 15 小时，完全自动形式化了证明。然后，在 @PietroMonticone 的大力帮助下，我设法建立了证明的蓝图版本。这是一个所有 LaTeX 文档部分变得互动并可以被检查和研究的版本。我们可以看到证明中的依赖关系并研究它们的关系。 在后处理阶段，我还使用了 Grok Heavy 和 Codex CLI，结合 GPT-5.2 的 xhigh 模式，逐行分析了形式证明。这对那些不是专业 Lean 4 程序员的人来说是一个很大的帮助。你可以真正内化证明的所有步骤。 我想总结一下我的印象以及我从这次经历中学到的东西。@vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei