Trellis 解决了自动形式化中可靠性与成本之间的平衡问题，做定理证明或形式化验证的开发者可以直接用这个工作流来生成 Lean 证明，值得关注其开源实现。
Trellis 是一个自动形式化系统，利用 LLM 智能体在确定性约束的工作流中，通过迭代优化自然语言证明，逐步推进 Lean 自动形式化任务。该系统受数学家对“严谨证明”的直觉启发——即证明的任何部分都可以被进一步详细阐述。Trellis 在有限预算下使用通用智能体实现了可靠的自动形式化，其专业化来自“严谨性”含义驱动的工作流，而非特定任务训练。论文还展示了该系统生成的 Ramsey 理论最新突破的端到端 Lean 形式化证明。
(Auto)formalization is supposed to be easy: Trellis process semantics for spelling out rigorous proofs
We present Trellis: an autoformalization system that leverages LLM agents in a deterministically constrained workflow to enforce incremental progress in Lean autoformalization tasks through iterative refinement of natural language proofs. Our approach is motivated by the common mathematician's notion of what it means to have a rigorous proof in the first place: namely, that it would be routine to elaborate any part of the proof in further detail. The result is a system which aims to achieve reliable autoformalization on a modest budget and with generalist agents, with specialization to autoformalization coming not from any task-specific agent training but instead from a meaning-of-rigor inspired workflow enforced by process semantics. We link to an end-to-end Lean formalization of a recent Ramsey theory breakthrough produced by the process.