（自动）形式化本应容易：Trellis过程语义展开严谨证明

我们提出了 Trellis：一种自动形式化系统，它在确定性约束的工作流程中利用 LLM 代理，通过自然语言证明的迭代细化来强制Lean自动形式化任务的增量进展。我们的方法的动机是普通数学家的概念，即首先拥有严格的证明意味着什么：即，更详细地阐述证明的任何部分都是例行公事。结果是一个系统，旨在以适度的预算和通才代理实现可靠的自动形式化，自动形式化的专业化不是来自任何特定于任务的代理训练，而是来自过程语义强制执行的严格意义启发的工作流程。我们链接到该过程产生的最近拉姆齐理论突破的端到端Lean形式化。