Summary (Overview)

• Trellis is an autoformalization system that uses LLM agents within a deterministically constrained workflow to translate rigorous natural-language mathematical proofs into fully formal Lean proofs.
• The system's core philosophy is that a rigorous proof is one where it is "routine to elaborate any step to any level of detail"—a definition Trellis operationalizes by enforcing incremental, meaningful refinement of a proof structure.
• Trellis successfully produced end-to-end Lean formalizations of two recent Ramsey theory breakthroughs: a conjectured-asymptotically-optimal $R(3,k)$ lower bound and a 50-year-old exponent barrier break for off-diagonal Ramsey numbers.
• The system runs on a modest budget with off-the-shelf generalist LLM agents, with no task-specific training; specialization comes from the process semantics, not the agents.
• The formalization of Bradac's paper finished in roughly two days, using 35% of a weekly ChatGPT Pro subscription budget, three days after the paper appeared on arXiv.

Introduction and Theoretical Foundation

The paper addresses a central problem in autoformalization: how to enforce incremental progress. The author argues that formalization of a rigorous argument should be "routine but tedious," implying that autoformalization should be tractable with existing publicly available LLM agents on a modest budget.

The fundamental theoretical foundation is a working definition of rigor:

A rigorous proof is one for which it is routine to elaborate any step of the proof to any level of detail.

This definition motivates the Trellis design: instead of training specialized agents, Trellis enforces a process that mirrors the methodical proof-decomposition workflow a mathematician would use when claiming "all the details can be filled in."

The paper identifies three failure modes of simpler autoformalization schemes:

1. False formalizations: claiming a complete Lean proof when it isn't (e.g., using sorry placeholders or unauthorized axioms).
2. Unfaithful formalizations: formalizing something, but not what corresponds to the actual paper target (e.g., a buried definition that undermines the meaning).
3. Empty wrapping: making "progress" by indefinitely deferring essential mathematical work to lemmas with increasingly long names—a single target proof file grew to thousands of lines without reducing the open-assumption set over ~150 cycles.

Methodology

Trellis operates over a proof tablet: a directed acyclic graph (DAG) of nodes, each with paired natural-language (LaTeX) and Lean sides. The process is governed by a deterministic kernel (35k lines of Rust, plus a 10k-line TLA⁺ spec) that owns all protocol state.

Verification Gates

Every node must pass three verification lanes:

• (a) Substantiveness: The LaTeX statement genuinely matches a claim used by the paper and represents a meaningful refinement (not a restatement of another node).
• (b) Correspondence: The Lean side genuinely corresponds to the mathematical meaning of the LaTeX side.
• (c) Soundness: The LaTeX proof is line-by-line checkable from available dependencies.

A fourth lane, Paperfaithfulness, verifies that nodes purporting to cover target theorems truly do so.

Key Design Features

• Human-protected semantic closure: The kernel computes the set of nodes whose Lean statements affect paper targets' meaning; only these are presented for human approval. The formalization's faithfulness depends only on this human-checked closure, not on agent reliability.
• Fingerprints: Content hashes of lane-relevant material. When an edit changes a fingerprint, the corresponding lane automatically reopens, ensuring verifier judgments can't be silently bypassed.
• Supervisor cycle: The kernel issues exactly one agent call at a time, with the worker being the only agent with write access. All Lean builds are checked in an isolated environment the worker can't tamper with.
• Scope ladder: In proof formalization, worker authority increases gradually: local (edit only the active node's proof + new helpers), restructure (coordinated edits in impact region), coarse-restructure (can change protected coarse nodes).
• Coarse focus: A distinguished subset of nodes (those present at phase transition) marks milestones; the kernel tracks monotone progress via "shallow-coarse-closure" counts.
• Authorized deviations: A fifth verifier lane allows paper-faithful departures (e.g., fixing typos) via durable deviation artifacts that must state the departure and give a rigorous return-to-faithful argument.

Empirical Validation / Results

The paper presents a complete end-to-end run formalizing Bradac's paper Nearly tight exponents for off-diagonal Ramsey numbers, which proves:

$$R(s,k) \geq c_s \frac{k^{s-2}}{(\log k)^{2s-6}} \quad \text{for } s \geq 4$$

Key Results

• Run statistics: 140 supervisor cycles, 156 nodes (119 theorem-like, 36 definitions, 1 preamble), 12,854 lines of Lean, all 5 paper targets formalized with no sorry or nonstandard axioms.
• Verifier pass rates:

• Natural language corpus: The LaTeX proof corpus grew to 15,196 words (vs. the paper's ~3,700), serving as "load-bearing glue" for the formalization.
• Monotone progress: The count of shallowly-closed coarse milestones rose monotonically from 0 to all 20, with one stall (cycles 80–101) that triggered a StuckMathAudit.
• Shared lattice structure: 119 of 156 nodes lie in more than one target's cone; 10 foundational nodes lie in all five targets, mirroring the paper's unified pseudorandom construction.

Theoretical and Practical Implications

• Process semantics over prompt engineering: Trellis demonstrates that reliable autoformalization can be achieved through deterministic constraints rather than task-specific training or sophisticated prompting. The kernel's semantic authority prevents verifier judgments from being bypassed.
• Progress as a machine-checkable property: By making substantiveness, correspondence, soundness, and Lean closure verifiable, Trellis turns "progress" from a vague notion into a concrete, checkable property of tablet state.
• Trust model: The system's correctness depends only on (1) machine-checked Lean builds and (2) human review of the semantic closure—not on any agent's reliability. Agents determine only whether Trellis reaches completion, not whether the result is sound.
• Complementary to existing tools: Trellis doesn't replace proof search or statement translation; it supplies a process layer around them, targeting the gap between paper proofs and final formal artifacts.

Conclusion

Trellis successfully demonstrates that autoformalization of substantial, cutting-edge mathematical papers is feasible with generalist LLM agents on a modest budget, provided the process enforces meaningful, incremental progress. The system's success on two recent Ramsey theory breakthroughs suggests that the "routine but tedious" nature of formalizing rigorous proofs can be operationalized through process semantics.

Future directions implied by the work include:

• Applying Trellis to a broader range of mathematical papers to assess generalizability.
• Exploring the system's potential for benchmarking and optimizing the fully automatic portion of autoformalization.
• Integrating Trellis-style process control with more sophisticated proof-search or tactic-prediction methods.

The author notes that Trellis's immediate aim—excellence at "autoformalize a given paper" with no guidance—differs from building reusable infrastructure, though it emphasizes and benefits from the availability of such infrastructure (e.g., Mathlib).