计算生物学家用Codex解决30年前提出的超立方体铺石数猜想

我最近用Codex解决了一个问题——这是我30多年前在第一篇论文中提出的。这令我十分兴奋，下文将解释其中的数学内容，以及我为此项目开发的一个工具：它帮助建立（人类可读的）LaTeX与（机器可读的）Lean之间的对齐。

为在证明定理的同时完成形式化，需在LaTeX中的定义、引理、命题、定理等与Lean中对应声明之间建立链接。为此，我创建了名为span的工具。

这一方法实现了Sinan Booeşaghi和Neuro Luebbert所倡导的愿景：“机器可读表示与面向人类叙事并存”。LaTeX ↔ Lean正是该愿景的完美例证。

span是什么？它提供一套受控词汇，用于构建“账本”（ledger），其中包含“跨度”（spans）：通过LaTeX标签链接到Lean中带完整命名空间的声明名。

span工具会校验账本是否结构良好：LaTeX标签必须存在，Lean声明名必须可解析，且生成的“面向论文的依赖图”须源自真实的Lean依赖关系，而非人工绘制的猜测。

span还支持验证AI生成的Lean定义是否符合证明本意，并有助于组织和可视化论文的整体结构。我发现它已成为我所有项目的必备工具。

我用它完成的是哪篇论文？数学问题是关于超立方体（hypercube）最优铺石数（optimal pebbling number）的猜想。该问题源于我本科就读加州理工学院时的一个暑期项目，合作导师是博士后Hunter Snevily（1956–2013）。

我在那篇论文中的贡献之一是定义了“最优铺石”，并提出确定超立方体最优铺石数的问题。

多年来多人研究过该问题，但它只是图论一个很小分支中的次要问题，长期未解并不意外。不过，David Moews（普特南数学竞赛史上首位满分获得者）也曾研究此问题。

我在研究生阶段多次思考该问题，甚至曾向Noga Alon当面提问；他当场给出了一个部分结果。最终发现，平凡的下界可通过概率方法的一个优雅应用达到匹配。

还有一个有趣的尾声：“合作至关重要”。这很有趣，因为该结论呼应了我近年在进化生物学中持续思考的一些想法。