(自动) 形式化本应简单：用于阐述严谨证明的 Trellis 过程语义

本文提出了 Trellis，一个利用大语言模型智能体的自动形式化系统。该系统通过在确定性约束的工作流中迭代细化自然语言证明，强制 Lean 自动形式化任务取得增量进展。其设计理念源于数学家对严谨证明的定义：即证明的任何部分都应能常规地展开为更详细的步骤。该方法旨在以适度成本和通用智能体实现可靠的自动形式化，其专业性并非来自特定任务训练，而是源于受“严谨性含义”启发并由过程语义强制执行的工作流。文中还展示了该系统生成的拉姆齐理论最新突破的端到端 Lean 形式化成果。