(Auto)formalization is supposed to be easy: Trellis process semantics for spelling out rigorous proofs
2026-06-08 • Artificial Intelligence
Artificial IntelligenceLogic in Computer Science
AI summaryⓘ
The authors present Trellis, a system that helps turn informal math proofs into formal ones using large language models (LLMs). Their method breaks down proofs step-by-step, making sure each part is clear and can be expanded if needed, similar to how mathematicians verify rigor. Instead of training special models for this task, they use a strict workflow inspired by the idea of mathematical rigor. They demonstrate their system by fully formalizing a recent result in Ramsey theory.
autoformalizationLean theorem proverlarge language modelsiterative refinementmathematical rigorRamsey theoryproof formalizationworkflow semanticsformal proof verificationdeterministic workflow
Authors
Wesley Pegden
Abstract
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.