Autoformalization of mathematical proofs remains unreliable, and existing systems often require expensive task-specific training or large compute budgets. The core difficulty is ensuring that an LLM agent makes incremental progress rather than getting stuck or producing invalid output.

Trellis uses LLM agents constrained by a deterministic workflow (process semantics) that enforces incremental progress in Lean autoformalization. The system iteratively refines natural language proofs, guided by the mathematical principle that a rigorous proof should be routine to elaborate at any point. Specialization comes from the workflow structure rather than task-specific fine-tuning, allowing generalist agents to perform autoformalization on a modest budget.

The system produced an end-to-end Lean formalization of a recent Ramsey theory breakthrough. The authors report that reliable autoformalization is achievable with generalist agents when constrained by meaning-of-rigor inspired process semantics.