formalization

本文重新思考了“状态”这一语言学概念，将其视为跨综合语言的一种系统性形态句法机制，在基于模板的模块化认知框架中将其形式化为语法模板上的集值函数，并提供了一个统一的计算学习理论解释。

包括ChatGPT和OpenAI的Sol在内的人工智能系统，已经驳斥并完全形式化了Erdős单位距离猜想，标志着人工智能辅助数学的一个里程碑。文章讨论了这一过程及其对数学证明验证未来的影响。

在Lean 4中对组合博弈论的形式化，涵盖游戏、nimbers和超现实数，基于Conway的工作。

本文介绍了MELD数据集，用于评估文本嵌入模型是否能够捕捉不同术语之间的数学等价性，并发现当前模型无法做到。本文提出了一种对比学习方法，用于对齐非正式和正式的数学表述，从而在非正式-正式检索任务以及自然语言任务上均取得改进。

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