Thomas Hales × GPT-6 Astra 提出 linchpin theorems：用少量可人工审计陈述锚定大规模 AI 形式化的语义可信度

Thomas Hales 于 10 月 16 日提交由 GPT-6 Astra 在其 prompting 下生成的《Linchpin Theorems》。核心观点是：proof assistant 只能确认形式 proposition 被证明，不能确认这个 proposition 就是人类真正想表达的数学；当 AI 批量 autoformalize 大型理论时，应挑选一组意义可由较少基础设施人工审计、但其 formal proofs 又连接到大规模下游结果的“linchpin theorems”。文章用 sphere packing、Lie algebra classification、regularity theory、Weil conjectures 与 complexity 等案例说明这种 semantic anchoring 思路。Hexagon provenance 明确标注文本由 ChatGPT-6 Astra 生成、没有人类 authorship，Hales 作为 contributor 提出任务与发布结果。