Trellis
Trellis is an autoformalization system that leverages LLM agents in a deterministically constrained workflow to enforce incremental progress on formalization 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 overseen by a deterministic supervisor.
📄Read the paper ★Code on GitHub
Formalized papers
-
The Strong Perfect Graph Theorem
This formalization was produced completely autonomously by Trellis, and is by far its largest run to date. It is a complete formalization of the Strong Perfect Graph Theorem — that a finite graph is perfect if and only if it is Berge, i.e. has no odd hole and no odd antihole as an induced subgraph — together with the full decomposition theorem for Berge graphs on which the proof rests: that every Berge graph is either basic, or admits a 2-join, a 2-join in its complement, an M-join, or a balanced skew partition. The terminal tablet has close to 1,500 nodes (roughly 1,100 theorem-like statements and 390 definitions) totaling around 530,000 lines of Lean; every proof obligation builds in the supervisor's isolated checker with no
[paper] [github] [formalization viewer]sorryplaceholders and only the standard axioms. The run took about six and a half weeks, from July 17 to September 1, 2026, over roughly 1,460 supervisor cycles. As with the other runs, no human input to the autoformalizer was given beyond the source manuscripts. -
Nearly tight exponents for off-diagonal Ramsey numbers
This paper was first formalized, completely autonomously, in two runs. The first covered v1 of the paper — its main lower bound together with the general off-diagonal, linear, near-diagonal, and multicolor Ramsey results — using 35% of the weekly usage budget of a ChatGPT Pro subscription, a prorated cost of around $18. After the paper was revised on the arXiv, a second run in Trellis's revision mode brought the formalization up to v3, whose main theorem is stronger: r(s,k) ≥ csks−1/(log k)2s−4 for s ≥ 3, in place of ks−2/(log k)2s−6 for s ≥ 4. Given only the old and new .tex files, Trellis diffed them itself, re-stated the affected target, rebuilt the proof tree beneath it, and re-verified the rest; the other four paper targets came through unchanged.
The paper has since been formalized a second time, independently and again completely autonomously, taken straight to v3 in a single one-shot run driven by only gpt-5.6-luna, a lightweight, low-cost model. That run also closes all five paper targets with no
[paper] main run: [github] [formalization viewer] · lightweight-model run: [github] [formalization viewer]sorryplaceholders and only the standard axioms, in a compact tablet of about 50 nodes, and illustrates how inexpensive such a run can be: even priced at gpt-5.6-luna's API rates, it would have only cost around $25. As with the other runs, no human input to the autoformalizer was given beyond the .tex manuscripts from the arXiv. -
Random volumes in d-dimensional polytopes
This formalization was produced completely autonomously by Trellis. It covers the paper's threshold in both directions: that exponentially many points chosen uniformly at random from an affine simplex suffice to fill all but a vanishing fraction of its volume, and the matching lower threshold showing that fewer than exp((γ−ε)d) samples leave a vanishing expected fraction covered, where γ is the Euler–Mascheroni constant. It also covers the generalization of the lower bound to arbitrary convex simplicial polytopes. As with the other runs, no human input to the autoformalizer was given beyond initially providing a .tex manuscript.
[paper] [github] [formalization viewer] -
Crossing numbers and hard Erdős problems in discrete geometry
This formalization was produced completely autonomously by Trellis. It covers the crossing lemma — that a simple graph on n vertices with at least 4n edges has crossing number at least e³/(100n²) — together with the discrete-geometric consequences the paper derives from it: the Szemerédi–Trotter bound on point–line incidences, the bound on the number of k-rich lines, and the O(n⁴⁄³) bound on the number of unit distances among n points in the plane. As mathlib does not have any plane graph machinery (e.g., no Euler's formula, and not even the polygonal Jordan curve theorem), Trellis automatically developed all of this machinery during this run. As with the other runs, no human input to the autoformalizer was given beyond an initial .tex file.
[paper] [github] [formalization viewer] -
Extremal collections of k-uniform vectors
This formalization was produced completely autonomously by Trellis. It covers the paper's extremal bounds for collections of k-uniform vectors over a finite field — the maximum number of distinct weight-k, and co-weight-k, columns a matrix of linear rank r can have, established for r large in terms of k and q — together with the rigidity of the extremal configurations and the generalization to finite sets of weight profiles. As with the other runs, no human input to the autoformalizer was given beyond an initial .tex file.
[paper] [github] [formalization viewer] -
Improving R(3,k) in just two bites
This formalization was produced while Trellis was still under very active development. The automated run reached a nearly complete state, but with a structure incompatible with newer Trellis features, so it was finished manually at the end: a human operator directed Codex to complete the repair along the paper-faithful route the system had already identified, without supplying mathematical content, Lean proof steps, or formalization-specific hints. The manual step did not change the statements of the public theorems. The formalization repo below includes checkpoints before and after this manual edit.
[paper] [github] [formalization viewer]
👥Trellis formalizations by others
How it works
Here is a high-level tour of how Trellis turns a paper into a machine-checked Lean formalization. The guiding idea, above, is that a proof is rigorous exactly when it would be routine to spell out any step in as much detail as one likes. Trellis operationalizes this: it forces a structured proof to be elaborated, step by step, until each remaining piece is easy to formalize — all under a deterministic supervisor that permits only genuine progress.
The proof tablet
Trellis works on a proof tablet: a directed acyclic graph of nodes wired together by Lean's import structure. Each node is either a definition or a theorem-like statement (a lemma, corollary, or helper) and carries two paired sides — a natural-language statement and proof in LaTeX, and a matching Lean statement and proof. The natural language is load-bearing: it is where the argument is decomposed and justified, before and as it is turned into Lean.
The whole system rests on keeping every node honest. Independent agents — each separate from the worker that wrote the node — judge it against three gates:
A fourth check, paper-faithfulness, applies to the few nodes meant to cover the paper's headline theorems. A run has two phases. In theorem-stating, Trellis drafts and refines the statements until every node passes its gates; a human then ratifies the Lean shapes of just the nodes those target theorems depend on (their semantic closure). Only then does proof formalization begin, where the goal is to close every Lean proof.
Enforcing progress
The hard part of autoformalization is not any single proof — it is guaranteeing steady progress across a run far longer than any agent's context window, without the agent quietly faking it. Trellis's answer is a rule with no escape hatch. Facing an open proof obligation, the worker may do only one of two things:
Because a too-hard step can only be broken into genuinely smaller sub-steps — never repackaged or deferred — the proof cannot stall or pretend to be finished. This is the “rigor as latent formality” idea made mechanical: keep spelling things out, and every step eventually becomes easy.
The supervisor cycle
All of this is driven not by a rotating sequence of prompts but by a deterministic kernel (written in Rust, with a TLA+ specification) that owns every decision and all protocol state — Lean build status, gate verdicts, and what each agent is permitted to touch. The agents around it — a worker, the verifier lanes, and a single reviewer that routes the worker — are ordinary general-purpose LLMs with no task-specific training. The kernel issues exactly one agent call at a time, only the worker can write to the tablet, and the authoritative Lean build runs in an isolated checker no agent can reach. The diagram traces one such cycle:
What Trellis trusts
This division of labor is what makes a finished formalization trustworthy even though the agents are not. Exactly three things are trusted, and nothing else:
Correctness
The supervisor's isolated Lean build and axiom check certify that every node's Lean proof really supports its Lean statement. Machine-checked; rests on no agent.
Faithfulness
A human ratifies the Lean shapes of the nodes the paper's target theorems depend on — their semantic closure. That, and nothing about the agents, ties the result to the paper.
Progress
The agents — worker, verifier lanes, reviewer — are trusted only to push the run forward. They decide whether Trellis finishes, never whether the result is sound.
That is the core. The paper gives more detail on the design — fingerprints and automatic re-verification, authorized deviations from the paper, and scope and “coarse focus” — and the source repository has the full TLA+ specification and implementation for anyone who wants to see the complete spec or implementation detail.