(Auto)formalization is supposed to be easy
stead that it is possible to “spell out all the details” of the argument to any required level. Indeed, the implicit claim is not even that it would just be possible to elaborate a given rigorous proof into a fully formal one, but that it should in some sense be routine to do so.
arXiv:2606.09674v1 [cs.AI] 8 Jun 2026
(Auto)formalization is supposed to be easy: Trellis process semantics for spelling out rigorous proofs
One promise of autoformalization is that the tedious work admitted by this claim can be alleviated by machines— that we should really be able to translate any rigorous mathematical argument into a truly formal one. On the other hand, however, the very premise that formalization of a rigorous argument should be “routine but tedious” should imply that autoformalization itself should be an unremarkable, completely tractable task not just when machines are brilliant but once they can follow and understand a correct argument. That is, autoformalization should be routine today, with existing publicly available LLM agents, on a modest budget, on problems of real substance.
Wesley Pegden1
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.
1
We present Trellis, a process semantics for autoformalization motivated by this view of why formalization should be routine (rather than motivated by, say, the observation that LLM agents are generally good at coding). In particular, Trellis works with an off-the-shelf generalist LLM, but in a highly structured process intended to mirror the methodical proof-decomposition workflow a mathematician might imagine when claiming that indeed, all the details can be filled in. The result is a workflow in which agents build and then maintain and expand an end-to-end proof structure held together by natural language proofs, as the process formalizes or refines individual pieces of this structure step-by-step. The fundamental problem this is an answer to is how to enforce incremental progress during an autoformalization task. Our answer is that progress can be enforced in our framework for the same reason that (auto)formalization is supposed to be easy: we can always refine parts of our proof until they are so spelled out that formalizing that piece is an easy task. The Trellis framework is designed to enforce a notion of refinement that maintains faithful correspondence to the formalization blueprint: the rigorous proof being formalized.
Introduction
Formalism underpins notions of rigor in mathematics, but usually not directly; when mathematicians talk of having a rigorous proof of a theorem, it is quite rarely because they have written out a specific type of proof object in a particular formal system. Instead, when claiming an argument is mathematically rigorous, the claim is really in-
Two complete Lean formalizations of recent Ramsey theory breakthroughs are now publicly available 1 Department of Mathematical Sciences, Carnegie Mellon University. alongside this draft, at h t t p s : / / m a t h . c m u . e 1
(Auto)formalization is supposed to be easy
du/˜ wes/trellis.php: Improving R(3, k) in just two bites by Zion Hefty, Paul Horn, Dylan King, Florian Pfender [Hefty et al.(2025)], and Nearly tight exponents for off-diagonal Ramsey numbers by Domagoj Bradač [Bradač(2026)]. The former achieves a conjectured-asymptotically-optimal R(3, k) lower bound; the latter breaks a 50-year-old exponent barrier for the general off-diagonal case. At the linked site, we provide viewers which allow easy browsing of both the Lean code generated by Trellis, and the natural language “glue” that holds the Trellis proof structure together.
The simplest of these failure modes is simply a process claiming to have a complete Lean [de Moura et al.(2015)] proof of something when it doesn’t; e.g., perhaps Lean does successfully build the project, but ‘sorry’ placeholders are used in various places in place of complete proofs. This is a failure mode that can easily arise in the simplest of experiments, where a deterministic script simply repeatedly asks an agent to continue until it reports that it is done (in which case the process terminates); an imperfect agent may well report done before it is truly finished. Devious instances of this problem class could involve using unauthorized axioms or tampering with the build environment. The natural solution to this problem is to have the autoformalization process independently check all Lean build claims, in an environment agents don’t have access to.
The formalization of the two bites paper took place over a period of two weeks when Trellis was under heavy development and thus when features and behavior were shifting from day to day. At the end of the period, the autoformalization had 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 paperfaithful route the system had already identified, without supplying mathematical content, Lean proof steps, or formalization-specific hints. The public formalization repo includes checkpoints before and after this manual edit.
Another common problem facing autoformalization schemes is the possibility that agents in an autoformalization process do formalize something, but not something corresponding in meaning to the actual formalization target. In particular, this problem can easily arise even with a strong adversarial model of Lean checking. In one target in an early experiment, the quantity of interest was the maximum size of a family. Early experiments even with strong agents frequently revealed cases where one unfaithful buried definition undermined the meaning of all paper targets. The natural solution to this problem is to have a system fix a set of approved target Lean statements before autoformalization begins.
The formalization of the Bradač paper took place with a much more settled codebase and thus we release the full end-to-end autoformalization repo [Pegden(2026b)] in which every cycle-checkpoint of the process is visible— that is, it is possible to inspect every edit made by the Trellis worker in the formalization process. This autoformalization finished in roughly two days, using 35% of the weekly usage budget of a ChatGPT Pro subscription; it completed on May 30, 2026, three days after Bradač’s paper first appeared on the arXiv.
2
After solving the first two problems, the risk is no longer false or unfaithful formalizations. The remaining problem one sees with weak systems is a failure to enforce real progress. One example of work without progress in our experiments running hardened but simplistic systems on hard problems is empty wrapping. An agent makes “progress” by telling their reviewing agent, “I’ve reduced the problem to this,” “I’ve reduced the problem to that,” etc., indefinitely deferring some essential part of the mathematical work to lemmas with increasingly long names. In one experiment, a single target proof file grew to thousands of lines, in which essentially every lemma derived its conclusion from an unproved hypothesis, and successive cycles renamed and repackaged that hypothesis—without ever reducing the open-assumption set—over roughly one hundred and fifty cycles.
Failure modes motivating the Trellis design
In early experiments with a range of simpler autoformalization schemes, we observed a range of failure modes; i.e., ways in which the process would claim to formalize an intended paper target when that claim was actually not justified. 2
(Auto)formalization is supposed to be easy
In Trellis, we address the first problem by adopting an ad- lemma, corollary, or helper), and every node carries two versarial stance for checking Lean builds; all Lean builds paired sides—a natural-language side written in LATEX and are carried out by the deterministic supervisor in an iso- a Lean side. lated environment the editing agent doesn’t have access To operationalize the notion that rigorous natural lanto. We address the second problem by having the process guage proofs can always be “elaborated”, Trellis builds settle Lean statements (including relevant definitions) rel- and then maintains the invariant that the Tablet is in a state evant to paper targets before formalization; these settled where every node has been judged by (separate) agents to statements are offered for human review and no changes satisfy the following three verification gates: to them are allowed during formalization without reopening human review. (a) Substantiveness: (Natural Language) The LATEX side of the node: (1) genuinely matches a statement used The third problem is the most interesting of the three (explicitly or implicitly) by the proof described by the problems; simple metrics like line counts and sorry counts paper, and (2) represents a meaningful refinement of are poor guides. Unproductive wrapping is great at inthe current Tablet; that is, it is not essentially the same creasing lines of code, and, of course, it only takes one in meaning as any other current node. sorry to take the place of the proof of any paper target. It is our solution to this problem that is motivated by our (b) Correspondence: (Natural Language and Lean): The Lean side of the node genuinely corresponds to the meaning-of-rigor viewpoint, that for rigorous natural lanmathematical meaning of the LATEX side of the node. guage proofs, it should always be feasible to elaborate them to any desired level of detail. We enforce progress (c) Soundness: (Natural Language): The LAT X side of E by enforcing that the process is always increasing meanthe proof contains a line-by-line checkable naturalingful detail in a proof’s decomposition. language proof with all needed dependencies available in Mathlib or in Tablet nodes imported by the node.
3
Rigor as Latent Formality
The first phase of the Trellis process is a Theorem-stating phase in which an initial directed acyclic graph (DAG) of Trellis nodes is built and refined until all nodes satisfy these three verifications. A fourth verifier lane Paperfaithfulness verifies that nodes that purport to cover target theorems in the paper being formalized truly do so. But we do not want to trust agent quality for inferring correctness of formalization, so Trellis computes the list of all nodes whose Lean statements affect the meaning of nodes that purport to cover paper targets, and presents these nodes for human acceptance. Only after this does the process proceed to the formalization phase2 .
The Trellis semantics rest on a working definition of what it means for a mathematical proof to be rigorous: A rigorous proof is one for which it is routine to elaborate any step of the proof to any level of detail. The Trellis process is designed to operationalize this definition: to orchestrate imperfect agents acting under the rules of a deterministic supervisor in such a way that details really do get “spelled out”, to the point that any part of the proof becomes easy to formalize. Importantly, we leverage the ability of agents to work with mathematics in natural language as much (if not more) than we leverage their ability to write Lean code; mathematics in natural language is the glue holding together our tablet of nodes as our process elaborates the paper we are formalizing.
In the proof formalization phase, an ideal step consists of writing a Lean proof for the Lean statement of a node, from its imports. Trellis then evaluates (in a separate environment the worker doesn’t have access to) whether this proof is valid conditioned on its inputs and doesn’t use any unapproved axioms. A fundamental reason autoformalization is hard, however, is that an agent will not always succeed at writing such a proof; frequently, this task
Trellis operates over a proof tablet: a directed acyclic graph (defined by Lean import structure). A node is either a definition or a theorem-like statement (theorem,
2 No changes are allowed to the human-approved semantic-relevant nodes without reopening human approval.
3
(Auto)formalization is supposed to be easy
will be considered too difficult to do all at once. In this situation, the Trellis process allows the agent another option: you may meaningfully enrich the DAG below this node, e.g., by adding helper nodes, but they will be required to pass the verification lanes substantiveness, correspondence, and soundness (soundness is waived for nodes already Lean-closed). The promise of this rule is that while agents may sometimes make mistakes, they should not systematically work in an unproductive way. When a worker refines the proof DAG rather than closing a Lean proof, it must, in essence, produce natural language certificates (checked by independent agents) that demonstrate its refined decomposition is meaningful (and, via substantiveness of new nodes, truly represents a refinement, rather than just the addition of pointless wrapper nodes). If a worker can only meaningfully refine a proof-step or formalize it, the Trellis philosophy goes, the worker cannot help but get to a point where formalization of one step of the proof eventually becomes a manageable task.
3.1
Contract enforcement prompt engineering
rather
The Trellis reviewer will never tell the Trellis worker to work on the Lean proof of a node that has not passed correspondence, because the deterministic kernel will reject such a directive and tell the reviewer to produce another one. And if a Trellis worker edits the Lean statement of a node to address a correspondence issue, it is the kernel that computes via Lean the set of upstream nodes whose own correspondence must be reopened for verification because of this change. The tablet is not merely a file layout: it is the progress ledger, and a local edit counts as progress only when it advances the tablet in a way allowed by the kernel-authorized scope chosen by the reviewer agent. That the two sides of a node are concrete files with a fixed shape is what makes their relationship checkable rather than conventional. The natural-language side of a node is a single statement block followed (except in the case of definition nodes) by a single proof block; the Lean side is a single principal declaration whose name matches the node, with an explicit marker separating the statement from the proof body. Dependencies are cited by name in both Lean and LATEX, via imports in Lean, and \noderef{} commands in LATEX. Deterministic structural checks enforce this shape, and the shape is then used by the deterministic kernel to decide when, e.g., soundness verification has to be reopened for nodes because of downstream changes to statements.
than
One could imagine trying to build an autoformalization system with the same motivation we describe here, engineered entirely out of a rotating sequence of prompts (e.g., in simplest form: to Agent 1: work on the Tablet: to Agents 2,3,4,. . . : Verify the work on the Tablet respects the verification lane rules, to Agent 1: Read the feedback from those agents and continue to work on the Tablet). In our experience, off-the-shelf agents still do not currently have the long-term horizon/perspective for this workflow to be reliable on difficult tasks orders of magnitude longer than the context window of any one agent.
3.2
Actors
Trellis separates roles that agentic workflows often conflate. Workers propose statements, dependencies, decompositions, and proof edits, and can also request different scope in the face of problems. Verifier lanes evaluate the semantic relations of §3; each lane is independent of the worker that produced the change and is judged by a single agent.3 The reviewer is a single adjudicator that consumes worker outcomes, accumulated verifier evidence, and the open-blocker set, and decides whether to continue locally, restructure, assign a blocker as a task, or escalate, within the confines of the rules enforced by the deterministic kernel. The human operator has a narrow task: provide the paper being formalized, and approve the Lean shape of
In particular, a workflow built only from agent prompts would let the judgments of verifier lanes from the distant past (but still for live Tablet nodes) be quietly bypassed. In Trellis, a reviewer agent directs the actions of a worker agent, but they are both tightly constrained by a deterministic kernel (leveraging durable long-term state memory) that owns semantic authority of the process. It tracks not only Lean build status but the results of verifier lanes, routing scope, Tablet permissions and state, etc.
3 A lane may instead be run as a multi-vote panel, where the kernel only records unanimous decisions and leaves split panels as Unknown.
4
(Auto)formalization is supposed to be easy
tion (polarity graphs of projective spaces) whose independent sets are counted with the container method. We pointed Trellis at five distinct headline theorems of the paper (thm:main, thm:off-diagonal-general, thm:k-Ck, thm:close, and the multicolor bound theorem MainTheorem : ∀ s : N, 4 ≤ s → ∃ c : R, 0 < c ∧ thm:multicolor) and otherwise left it alone. A sin∀ k : N, 2 ≤ k → gle off-the-shelf general-purpose reasoning model filled c * ((k:R)ˆ(s-2)) / ((Real.log (k:R))ˆ(2*s-6)) ≤ (RamseyNumber s k : R) every role—worker, reviewer, and all four verifier lanes— with no task-specific training.4 This run never invoked RamseyNumber semantic-closure definition the separate per-file deviation lane of §5.4: it followed The two-color Ramsey number r(s, k) is the least n such that the paper’s exact path throughout, needing no authorized every graph on n vertices contains a clique of size s or an inde- departure. MainTheorem paper target For any s ≥ 4 there is a constant cs > 0 such that for all k ≥ 2, k s−2 r(s, k) ≥ cs . (log k) 2s−6
pendent set of size k.
noncomputable def RamseyNumber (s k : N) : N := sInf {n : N | RamseyProperty s k n}
Outcome. The run halted cleanly after 140 supervisor cycles with all five paper targets formalized. The terminal tablet has 156 nodes (119 theorem-like, 36 definitions, one preamble) totaling 12,854 lines of Lean. Every one of the 119 proof obligations builds in the supervisor’s isolated checker with no sorryAx or other nonstandard axiom dependencies.
RamseyProperty semantic-closure definition R(s, k, n): every simple graph on n vertices contains a clique of size s or an independent set of size k. def RamseyProperty (s k n : N) : Prop := ∀ G : SimpleGraph (Fin n), (∃ S : Finset (Fin n), G.IsNClique s S) ∨ (∃ I : Finset (Fin n), Gc .IsNClique k I)
Refinement, not redefinition. Figure 2 tracks three quantities across the whole run: the total node count, the number of nodes passing every verifier lane (correspondence, substantiveness, and soundness), and the number of nodes Lean-closed in the isolated checker. Two regimes are visible. In theorem-stating (through cycle ∼25) the tablet settles at 48 nodes and the verifier-lane curve climbs to meet the total, as drafted statements pass their gates; the human then approves the target-semantic Lean shapes and the run crosses into formalization. There, the central observation is the shape of the Lean-closure curve. Our process semantics prohibit the lane curve from straying indefinitely from the node total, as every introduced node is required to clear substantiveness, correspondence, and soundness as it is added. In particular, when a worker cannot close a Lean obligation outright, its only sanctioned alternative is to spell the step out further, and substantiveness (Clause 2) forbids the spelling-out from being a vacuous repackaging. The growth is genuine decomposition, not the empty wrapping that defeated the simpler pipelines of §2. Table 1 quantifies the pass rate of verifier lanes in the Bradač paper run.
Figure 1. The human-protected core of one of the five targets (Figure 4) from Bradač’s paper: the main theorem’s statement and Lean declaration, with the two definitions in its kernelcomputed semantic closure—the only nodes the target’s meaning depends on, and the only Lean shapes a human ratifies. The faithfulness and correctness of the final formalization is only subject to the faithfulness of the nodes in this semantic closure, without any assumptions on the reliability of LLM agents.
the kernel-computed set of nodes relevant to paper targets at the phase transition from theorem stating to proof formalization.
4
Recursive Refinement in Practice
We illustrate the process on a single end-to-end run: an unguided formalization of Bradač’s recent paper Nearly tight exponents for off-diagonal Ramsey numbers [Bradač(2026)]. The paper is short but cutting-edge, 4 The model used here was GPT-5.5 xhigh, which likeimproving the half-century-old Spencer lower bound wise filled all roles in the other formalization linked with this on off-diagonal Ramsey numbers, showing R(s, k) ≥ manuscript [Pegden(2026a)]. Trellis has also been run successfully with s−2 2s−6 cs k /(log k) for s ≥ 4, via an algebraic construc5
(Auto)formalization is supposed to be easy
total nodes passing all verifier lanes Lean-closed theorem-like definitions
nodes
150
100
20
40
60
80
100
120
140
supervisor cycle
natural-language proof words
Figure 2. Verification and Lean-closure progress over the run. Total nodes (definitions in blue, theorem-like in orange) and the count passing all verifier lanes (solid) rise together—every committed node is lane-clean—while Lean-closure (black) lags, catching the total only at termination. The human-approved scaffold barely moves (28 → 37); the theorem-like population grows 20 → 119. total NL proof words words in un-Lean-closed nodes words backed by Lean
15, 000
15,196
proof formalization
0 20
40
60
calls
pass
pass-rate
substantiveness correspondence soundness
17 20 21
14 15 19
117 113 4
113 109 4
94.8% 93.2% 92.0%
total
58
48
234
226
93.8%
The decomposition is visibly recursive. The main theorem, for instance, was not closed in one shot; the worker reduced it through a chain of substantive helpers it had to state and justify along the way—a dyadic Galois-field scaling lemma, the polarity-graph setup and parameter bounds, an eigenvalue bound, a large-k comparison, and a finite-range absorption step—each a real sub-obligation that itself cleared the gates. The technical heart of the argument, counting independent sets in the construction, accreted the largest single cluster of machinery (a family of some two dozen “bad-tuple” counting nodes). The last recorded worker action is representative: it closed thm:off-diagonal-general by introducing one final Lean-closed numerical-absorption helper and using it for the range and Ramsey comparisons.
6, 136 5, 000
1
pass
mands a line-by-line checkable argument for every node. The total grows to 15,196 words as statements are decomposed and justified; for comparison Bradač’s paper is approximately 3,700 words, excluding the introduction and bibliography. The diagnostic curve is the un-Lean-closed share, which can be taken as a crude measure of the unfinished Lean obligation; note that it is a unique feature of our method based on natural-language elaboration that we get this kind of concrete metric of remaining work.
10, 000
thmstating
calls
Table 1. Per-node verifier-lane activity over the run on the Bradač paper, split by phase. A call is one verdict the lane returned for a node; pass counts the Pass verdicts among them (re-verification after a fingerprint drift is a fresh call). Note that soundness verification is waived for nodes introduced already lean-closed, as was the case with the majority of new nodes introduced in this run during the proof-formalization phase.
proof formalization
0 1
proof formalization
Lane
50 thmstating
theorem stating
156
80
100
120
140
supervisor cycle
Figure 3. The natural-language proof corpus through the elaboration process. By the end of theorem stating the total LATEX proof words (green) already exceed 6,000—more than the target paper’s ≈3,700 (excluding introduction and bibliography). Through formalization the total grows to 15,196, while the share in un-Lean-closed nodes (red) trends to zero: every proof obligation ends supported by a valid Lean proof. The red tick marks the peak un-Lean-closed backlog of 6,136 words.
From prose to Lean. Figure 3 views the same run The shape of the finished artifact. Figure 4 renders through its natural-language proofs. Trellis treats LATEX the terminal tablet as the kernel sees it: a single DAG proofs as the load-bearing glue—the soundness lane de- whose deepest import chains run 17 steps from a primitive definition up to a paper target. Figure 1 shows Opus 4.7 max and Gemini 3.1-pro preview in various roles. the meaning-bearing root of that DAG concretely—the 6
(Auto)formalization is supposed to be easy
definition (36)
theorem-like (119)
semantic closure (4)
bold = coarse (47, present at the phase boundary)
vs.
paper target (5)
faded = fine (added during formalization)
thm:k-Ck
thm:multicolor
thm:main
thm:close
thm:off-diag
Figure 4. The terminal proof tablet (156 nodes), laid left-to-right by import depth; edges are direct Lean imports. Squares are definitions, circles theorem-like nodes, labeled red pills the five paper targets; boldly drawn nodes are the 47 coarse nodes fixed at the phase boundary, the faded ones the fine scaffolding added during formalization. The four enlarged red squares are the targets’ kernel-computed semantic closure—the only nodes the targets’ meaning depends on, and thus the human-protected core: of all 156 nodes, only edits to these four (plus the five targets) can change what the targets mean.
natural-language/Lean pair for the main theorem and for the two definitions in its semantic closure, which are exactly the shapes a human ratifies before formalization proceeds. The structure is not a tree of five independent proofs but a shared lattice—119 of the 156 nodes lie in more than one target’s cone, and 10 foundational nodes lie in all five—which mirrors the paper itself, where one pseudorandom construction underlies every headline bound.
5
lines of python plumbing for agent calls and so forth. Our source repo at [Pegden(2026c)] also includes a detailed TLA+ [Lamport(2002)] spec of the process of 10k lines. In this section we aim to clearly describe a simplified view of the most salient details of process semantics and implementation.
5.1
The Tablet
In a Trellis autoformalization run, the Tablet of Lean/LATEX nodes is itself a git repository. Among all agents in the process, only the worker agent has write access to the Tablet (the deterministic supervisor does as well), and only the deterministic supervisor has write access to the .git directory controlling history. Worker edits
Details of the Trellis design
Our Trellis implementation sits in a kernel of (at time of writing) 35k lines of Rust code, supported by another 20k
7
(Auto)formalization is supposed to be easy
StuckMathAudit: the kernel interposes it when proof formalization stalls; it writes a recovery plan for the reviewer.
AUDIT
REVIEWER adjudicates split blockers & routes next worker
REVIEWER
isolated build · axiom check · type-surface fingerprint
CHECKER SERVER
worker takes ONE action (scope+directive)
WORKER
KERNEL
VERIFIER LANES
recovery plan
S TART C YCLE: cycle++
kernel validate: shape check · Lean build · axiom check
Valid +delta
reconcile lanes & recompute global blockers + reopen.
commit ckpt. (→S TART C YCLE)
substantiveness (node) correspondence (node) soundness (node)
new cycle
Figure 5. One supervisor cycle in proof formalization. The kernel issues exactly one agent call at a time; time runs left to right and each swimlane is the actor the kernel consults. Solid arrows are the normal control flow; the black dashed arrow carries outcomes that bypass the verifier lanes straight to the reviewer; the arrow returning to the worker is an Invalid retry. A green double line marks each step that consults the isolated checker server, which has its own lane: the worker test-builds its edits there, and the kernel’s validation runs the authoritative build, axiom check, and type-surface fingerprint there. The red dashed detour in the top lane is the occasional StuckMathAudit agent, which the kernel interposes when formalization stalls and which only advises the reviewer. Of the agents, only the worker can write to the Tablet.
5.2
accepted by the deterministic supervisor are committed as checkpoints (git commits) to the Tablet git repository; rejected edits are rolled back. We refer to any node failing one of the verifier lanes as a blocker; a clean checkpoint is a git checkpoint with no blockers. The initial theorem stating phase is the phase where the process aims to reach a clean checkpoint. After that, in proof formalization, the process aims to close all Lean proofs with limited drift from clean checkpoints. That is, work may involve changes to nodes that temporarily invalidate verifications of other nodes, but we expect to be able to repair these issues and get back to a clean checkpoint, otherwise the reviewer can choose (or be forced to choose) LastClean, a git rewind of the tablet to the last clean checkpoint.
The supervisor cycle
Within a phase the supervisor advances the run in cycles, the pipeline of Figure 5. The supervisor is the process that drives the deterministic side of the run; at its core is a kernel—a state machine, written in Rust and specified in TLA+ , that owns all protocol state and makes every decision (the KERNEL row of the figure)—which the supervisor runs while also performing the I/O the kernel abstracts away: dispatching each stochastic agent in a sandbox, and running the authoritative Lean build through an isolated checker the agents cannot reach. The remaining rows of the figure are the agents the supervisor consults. The supervisor keeps exactly one agent request in flight at any moment and commits a checkpoint only at the close of the cycle. A cycle begins by choosing an active node together with a scope—the set of nodes the worker
8
shallow-closed milestones
(Auto)formalization is supposed to be easy
C6
✓ C4
C5
✓
10 5 0 50
75
100
125
supervisor cycle (proof formalization)
✓
C2
progress stalls ⇒ StuckMathAudit
15
26
ff
fe
20
Figure 7. Shallow-coarse progress in the run on the Bradač paper: how many of the 20 coarse milestones are fully shallowcoarse-closed, by cycle. It rises monotonically to all 20; the shaded plateau (cycles 80–101) is a stall that tripped a StuckMathAudit.
C3
fb
✓ C1
cal work is completed. Figure 6. Coarse focus. Large nodes are coarse (already present when the proof formalization phase begins), small ones fine (added during proof formalization); green = Lean-closed, white = open. A coarse node is shallow-coarse-closed (✓) when it and everything reachable along import edges (pointing downward, toward dependencies) up to the next coarse node is closed. Shaded regions are such closures; they overlap at shared fine nodes (fb , fe ). C5 is Lean-closed but not shallow-coarse-closed, since ff is open.
The deterministic checks above are run in an isolated checker: a long-running, supervisor-owned server reached over a local unix socket. The checker derives the build target from its own runtime root and always compiles the supervisor’s authoritative workspace, into which the worker’s edited Tablet sources are first mirrored by a hardened, fingerprint-cached sync. The same checker is consulted by two clients of different standing: the untrusted worker calls it during its turn to test-build and iterate on its own edits, while the kernel calls it for the authoritative validation of a submitted edit. Because both routes compile the identical supervisor workspace, the worker’s use is a convenience that cannot move the verdict; the kernel’s call is the binding one. The checker performs the build-bearing checks—the isolated build of a node, the axiom check, and the Lean type-surface fingerprint— while the purely structural shape check and the approvedaxiom policy decision remain in the kernel, which only consumes the checker’s reported facts. The conditional character of the build is exactly as above: when a node’s local closure reaches an imported Tablet theorem, the checker records it as a boundary helper assumed at its stated type rather than re-elaborating its proof, and the kernel verifies that boundary statement against the imported node’s ratified statement, so that node-local checks compose into the global guarantee. An important design principle motivates the use of the checker server: we want
is permitted to edit—and a directive fixing the kind of edit expected, such as closing the active node’s own proof or restructuring the support beneath it. The worker returns a single edit to the Tablet, and the supervisor checks it deterministically before any other agent sees it: a shape check that the touched files have the required form (one principal Lean declaration named for the node, a single LATEX statement block, and dependencies cited both by Lean import and by \noderef); an isolated build in which the Lean sources are recompiled from scratch in isolation, against a workspace the worker cannot tamper with; and an axiom check that the build rests on nothing beyond a small approved axiom set, with no sorry hidden in a node claimed closed. Isolated builds check whether edited Tablet nodes build correctly conditioned on the truth of their imported nodes (e.g., if the imported node statements were considered axioms). In this way, we can work locally but be finished globally once all lo-
9
(Auto)formalization is supposed to be easy
isolated, independent checks of the worker’s work, but we also want the worker to have access to exactly the same checks that will be used to accept or reject the worker’s delta, so that cycles are not wasted on worker cycles that were genuinely productive but rejected because of differences between worker and supervisor build environments or assumptions.
The supervisor computes it by walking outward from the node’s principal declaration through the constants its type mentions, transitively, keeping what determines meaning and dropping what does not. From a theorem or lemma it takes the statement (its type) but never the proof term, so a lemma used only inside another node’s proof never enters that node’s type-surface; from a definition it takes both the type and the value, since a definition’s value is part of its meaning (D := 3 becoming D := 4 must re5.3 Verification and fingerprints open everything that transitively uses D); from an inductive it takes the type together with its constructors. The An edit that changes Tablet content carries a semantic walk stops at the Mathlib boundary: a referenced constant delta. When there is a delta, the supervisor dispatches the defined outside the Tablet is recorded by name but not unchanged nodes to the verifier lanes, independent agents folded, with shifts in the external library caught instead that each certify one semantic relation. The three per- by the pinned toolchain and lake-manifest hashes. The node lanes are substantiveness—the node’s LATEX state- collected surface is then hashed—canonicalizing away ment is a claim the paper genuinely uses, at the paper’s source-position metadata and bound-variable names, but strength, and is not in essence a restatement of another not implicit-versus-explicit binder information—to give node; correspondence—the node’s Lean signature cap- the Lean component of the correspondence fingerprint. tures the full, precise meaning of its LATEX statement; Because proof terms never enter, rewriting or reorganizand soundness—the node’s LATEX proof is a line-by-line ing a Lean proof changes no correspondence fingerprint; checkable argument from the statements of the nodes it only a change to a statement’s type or a definition’s value, cites. An approving verdict is stored with an approved on the node or on something its statement transitively fingerprint, a content hash of exactly the material rele- uses, reopens correspondence. vant to the lane’s judgment (Table 3); the supervisor keeps each node’s current fingerprint beside it and, whenever an This same type-surface walk defines the paper targets’ edit elsewhere makes the two diverge, it automatically re- human-protected semantic closure (Figure 1): the set opens that lane, returning the node to the blocker set.5 of Tablet declarations reached by walking outward from Having run the lanes and recomputed every such reopen- each target declaration—taking statement types but never ing, the supervisor rebuilds the global blocker set and proof terms, definition values, and inductive construchands the cycle to the reviewer, the single adjudicator that tors, and stopping at the Mathlib boundary, whose conresolves each node still Unknown and chooses where the stants are treated as pinned (by the toolchain and lakemanifest hashes). This closure is the trusted base of the worker goes next. formalization, human-approved as a frozen package at the What the correspondence fingerprint hashes from the phase transition. The kernel will not mark a run ComLean side is not the whole declaration but its type-surface: plete unless every paper target and every declaration in the part that fixes the statement’s mathematical meaning. this closure stands in its approved state with no open blocker; and any accepted edit that changes one of these 5 Downstream reopening of this kind is what maintains correspondence, soundness, and—per target—paper-faithfulness, whose finger- declarations—its signature, a definition’s value, or which prints draw in the imported type-surfaces, cited statements, and covering declarations its type-surface draws into the closure— sets that a change elsewhere can disturb; keeping these current is what alters that node’s fingerprint and deterministically reopens holds the DAG formalizable and faithful to the paper. Substantiveness is A a deliberate exception: its fingerprint is node-local—a node’s own L TEX the human-approval gate. No reviewer decision or later statement judged against the paper—so a downstream edit does not re- worker edit can route around this gate, the isolated Lean open it. It serves chiefly as a guard against unproductive decomposition build, or the axiom check, so the faithfulness of the result (Clause 2 of §3) rather than a relation the rest of the DAG must preserve, depends only on this human-checked closure and never on and reopening it on downstream changes, though a natural alternative, the reliability of any agent. has in our experience seemed unnecessary.
10
(Auto)formalization is supposed to be easy
5.4
Authorized deviations
The substantiveness lane requires every node’s statement to be a claim the paper genuinely uses, which by default forces the formalization onto the paper’s exact path. Occasionally, however, it is natural to allow a node’s statement to differ mathematically from the paper’s path in some way (e.g., because of an error in the paper, or because formalization favors a slightly different route); a constant changed in a proof, a strengthened hypothesis, a weakened conclusion, or an alternate intermediate statement that a later step absorbs. Trellis admits such a departure only via an explicit, authorized, durable deviation artifact. A deviation lives in a single LATEX-only file under reference/ that must state the departure, name the nodes it affects, and give a rigorous return-to-faithful argument: a concrete account of where the difference is absorbed so that the formalization rejoins a paper-faithful step. Each deviation must be self-contained. Authorization is decided by a fifth verifier lane, distinct from the four of §3. Where substantiveness, correspondence, and soundness are per-node and paper-faithfulness is per-target, the deviation lane is per-deviation-file: an independent agent reads the one reference file together with the relevant paper context and DAG nodes and decides whether that single departure is authorized—a paper-bound check the kernel tracks under its own blocker (kernel Deviation kind and object), running within the paper-verification stage ahead of per-node substantiveness. The tie to node judgment is what gives a deviation force. A node whose statement departs from the paper passes substantiveness only by claiming the deviation that licenses it, and substantiveness then judges the node, the paper, and its claimed deviations together; a claim on an unauthorized deviation does not satisfy the lane. To introduce such a node the worker writes the reference file, registers the deviation, and records the claim on each affected node in one move; to retire one it deletes the file and drops the claims. Deviation files carry their own fingerprints, so editing one reopens its authorization exactly as editing a node’s content reopens its per-node lanes— the worker cannot quietly alter an authorized departure and keep the verdict. The importance of this system is that it provides durable kernel-tracked authorizations to deviate from the paper;
in the presence even of minor mathematical typos, a system like Trellis which aims to ground formalization on a paper-faithful path could struggle with inconsistent or contradictory decisions by agents tasked with that grounding.
5.5
The reviewer and audits
The cycle then closes at the reviewer. Normally the supervisor commits the new state as a checkpoint and the next cycle begins; but if the worker’s edit fails validation—an Invalid outcome—the supervisor discards it and re-issues the same request as a fresh attempt, retrying a bounded number of times within the cycle before escalating to the reviewer regardless. Three other outcomes bypass verification and reach the reviewer directly (the dashed path in Figure 5): the valid no-delta edit above, an action the worker abandons as Stuck because it cannot proceed under the current scope, and an action it returns as NeedsRestructure, declaring the present decomposition itself wrong and asking for broader scope. The top lane holds a read-only audit role the kernel interposes only under specific conditions, never on an ordinary cycle. StuckMathAudit is triggered at signs of stagnation; e.g. when too many cycles pass without a clean checkpoint while a soundness or substantiveness blocker remains open; it studies the stalled region and writes a recovery plan for the reviewer. Like all other non-worker agents, it does not edit the Tablet directly; it can only advise the reviewer and/or call for a git rewind of the Tablet to a previous state.
5.6
Scope and coarse focus
Each worker burst is granted a bounded scope: the set of already-present nodes it may edit that cycle. The reviewer selects a mode, and the kernel both bounds and enforces the choice (Table 5). In theorem stating the modes are global, which authorizes all nodes, and targeted, which authorizes only the bidirectional dependency closure— the impact region—of a chosen node. In proof formalization the modes form a ladder of increasing authority: local permits editing only the active node’s own Lean proof together with new helper nodes in its sup-
11
(Auto)formalization is supposed to be easy
port cone; restructure permits coordinated edits across an explicitly enumerated subset of the focus node’s impact region, including signature changes to helpers introduced during formalization; and coarse-restructure additionally permits signature changes to the protected coarse nodes fixed at the phase boundary, and is the only mode under which a node’s human-approved correspondence may be reopened. Throughout, the kernel distinguishes the broad scope envelope a mode could authorize from the explicit authorized nodes the reviewer actually hands the worker—which for the restructuring modes must be a non-empty subset of the envelope, and which never implicitly includes the active node, since that node is a scope anchor and not itself edit permission. Before dispatch the kernel rejects any out-of-envelope or out-of-cone authorization, an empty authorization under a restructuring mode or a non-empty one under local, and any blocker assigned to a worker whose scope cannot reach it; after dispatch it rejects any burst whose file delta touches a node outside its authorized set. Scope is constrained further so that the run advances monotonically (Figure 6). A distinguished subset of nodes—the coarse DAG, the set of all nodes present when the run enters proof formalization—marks the principal milestones, the remaining nodes being the fine scaffolding beneath them. For each coarse node the kernel computes its shallow-coarse-closure: the node is shallowly closed when it, and every dependency reachable along fine import edges, is present and closed, where the walk halts at any other coarse node rather than descending through it. One milestone’s closure is thus independent of the milestones beneath it. A single coarse node is the active anchor: it confines every focus and authorization that cycle to its support cone, and is locked—the reviewer cannot advance it—until it is shallowly closed and free of blockers. The kernel’s progress measure is the number of shallowlyclosed coarse nodes against the committed state, and it tracks how many checkpoints have passed since that count last rose. The utility of this progress measure is that new coarse nodes are never introduced by refinement, so enforcing monotone progress with respect to this measure is feasible. When the count stalls beyond a fixed threshold the kernel interposes a StuckMathAudit in place of the next reviewer turn. A stronger no-regression rule records the coarse nodes ever observed shallowly closed and for-
Table 2. Worker outcomes and the kernel’s response. A semantic delta is a content change or any non-Same structural update; no-delta Valid skips verifiers. Stuck/NeedsRestructure roll the worktree back to the active base before escalating. Outcome
Kernel action
Next stage
Valid (+ delta) Valid (no delta) Invalid
apply, schedule verifiers apply, skip verifiers retry if attempt < thr. (2) else escalate w/ context Stuck rollback; retry-or-escalate NeedsRestructure rollback; no retry
Content the fingerprint hashes the node’s own content LATEX statement LATEX proof Lean type-surface (its own signature) Lean proof body content of the nodes it depends on Lean type-surface imported definition’s LATEX statement cited node’s LATEX statement
subst.→corr→. . . Reviewer Worker Reviewer Worker / Reviewer Reviewer
subst.
corr.
sound
✓
✓
✓ ✓
✓
✓ ✓ ✓
Table 3. What each per-node verifier lane’s approved fingerprint hashes (subst. = substantiveness, corr. = correspondence, sound = soundness). A lane reopens on a node whenever any content it hashes changes; because a node’s Lean type-surface includes the types of everything it imports, editing one node’s signature reopens correspondence on every node that imports it, while reorganizing a Lean proof body reopens nothing.
bids advancing the active anchor while any of them has lost closure, pinning work on the regressed material until it recovers; after a configurable threshold is passed, the kernel can use git to rewind the Tablet to the state at which the currently active anchor was first chosen. In the run on the Bradač paper this measure is well behaved (Figure 7): the count of shallowly-closed coarse milestones climbs monotonically from 0 at the start of formalization to all 20 at the end, pausing only for one extended plateau (cycles 80–101) that tripped a StuckMathAudit that produced concrete advice for the reviewer. What’s left out here. We omit configurable cadence constants (audit cooldown/re-audit intervals, retry thresholds), the orphan-cleanup detour scheduled when a delta 12
(Auto)formalization is supposed to be easy
Table 4. Reviewer directives and the kernel guards that bound them. All adjudications require the target to be in the just-voted latest * review frontier with status Unknown.
5.7
Trust model
It is worth stating precisely what Trellis trusts, and for what. We trust the supervisor’s deterministic checks—the Directive Key guard isolated Lean build and the axiom check—to certify that C ONTINUE (lo- authorized nodes = ∅; edits active each node’s Lean proof genuinely supports its Lean statecal) node only ment; this is machine-checked and rests on no agent. We task blocker worker scope must cover the carrier (Local trust the human review of the paper targets’ semantic closoundness carve-out for active node) sure (Figure 1) to certify that the formalization is faithful reset blocker theorem-stating only; current state Fail only restructure authorized nodes ̸= ∅ ⊆ scope env. ∩ to those targets: a human ratifies the Lean shapes of exanchor cone actly the declarations the targets’ meaning depends on. LastCommit / exclusive with partition; LastClean needs a And we trust the quality of the agents’ work—workers, LastClean prior clean checkpoint A DVANCE legal only when blockers = ∅; routes to huverifier lanes, and the reviewer—only for progress; no P HASE / D ONE man gate / Complete trust in any agent, the verifier lanes included, is required to trust that a completed formalization is faithful to its tarTable 5. The scope ladder: the existing nodes a worker may gets. Faithfulness and correctness thus reduce to the first edit each cycle. The reviewer picks a mode; the kernel bounds two; the agents determine only whether Trellis reaches a the envelope, and the reviewer hands the worker an explicit completed state, not whether that state is sound. authorized nodes subset of it. The active node is a scope anchor, not edit permission. Modes carry the orthogonal closure directives of Table 4. Mode
Authorizes nodes)
6
Relation to Prior Work
(existing Notes
Work on automated and neural theorem proving has produced systems that search for proof — terms [Polu and Sutskever(2020)], integrate learned modbidirectional depels with automated provers [Jiang et al.(2022)], repair closure whole proofs with language models [First et al.(2023)], or retrieve premises to prove theorems inside proof authorized = ∅ assistants [Yang et al.(2023)]. Benchmarks such as may re-sign helpers miniF2F [Zheng et al.(2022)] have made formal proof generation more measurable, and Lean with its mathematonly mode that reical library has made large-scale formalized mathematics opens approved correpractically accessible. A parallel line studies autoforspondence malization itself. One strand frames it as a long-term, cleanup cleanup the cleanup target node lint / substitution learning-driven route to general mathematical reasoning, in which a system bootstraps the ability to read and formalize mathematics largely from data [Szegedy(2020)]; orphans nodes, and many other implementation details, another shows empirically that few-shot LLMs can the authoritative reference for which are the Rust kernel translate individual competition-problem statements into (engine.rs, model.rs) and the TLA+ specification formal specifications, the resulting data then improving [Pegden(2026c)]. a neural prover [Wu et al.(2022)]. Trellis departs from both: it adds no task-specific training—its specialization is the meaning-of-rigor motivated process semantics, not a learned formalization model—and its unit of work is a whole paper’s proof, decomposed and Lean-closed end to theorem stating global all present nodes targeted impact region of the focus proof formalization local active node’s proof + new helpers restructure enumerated subset of the impact region coarse-restr. as restructure, + protected coarse nodes
13
(Auto)formalization is supposed to be easy
end, rather than an isolated statement.
this document.
Trellis is complementary. It does not replace proof search, tactic prediction, or statement translation. It supplies a process layer around them. Its target is the gap between a paper proof and a final formal artifact: the long interval in which the system must decide whether partially formalized statements, lemmas, and proof sketches are genuine progress. In that sense, Trellis is closer to a workflow semantics for mathematical refinement than to a standalone prover. It should be noted also that the immediate aim of Trellis is excellence at the task “autoformalize a given paper” with no guidance, which is quite different from the task of building useful infrastructure [The mathlib Community(2020)], where every choice made is essential for further utility. Needless to say, the feasibility of the task Trellis aims for excellence at is tied to the availability of suitable infrastructure6 , and in this way emphasizes, rather than obviates, the value of such infrastructure7 . The closest conceptual relatives are human-in-the-loop formalization environments and agentic proof assistants. Kontorovich [Kontorovich(2025)] describes a closely related “quasi-autoformalization” workflow, in which a decomposer, translator, solver, and conductor help turn mathematical prose into Lean, with human intervention available when useful. Trellis shares this basic motivation but, at least in its form today with a focus on end-toend formalization, assigns complete semantic authority to a deterministic kernel rather than to an agentic conductor. The goal is to make progress a machine-checkable property of the tablet state—through substantiveness, correspondence, soundness, and Lean closure. It also provides a way of optimizing and benchmarking the fully automatic part of autoformalization, even when imagining implementations that keep a human in the driver’s seat.
References [The mathlib Community(2020)] The mathlib Community. The Lean mathematical library. In Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020. [Bradač(2026)] Domagoj Bradač. Nearly tight exponents for off-diagonal Ramsey numbers. arXiv preprint arXiv:2605.28793, 2026. [de Moura et al.(2015)] Leonardo de Moura, Soonho Kong, Jeremy Avigad, Floris van Doorn, and Jakob von Raumer. The Lean Theorem Prover (System Description). In Automated Deduction - CADE-25, 2015. [First et al.(2023)] Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and repair with large language models. In Proceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, 2023. [Hefty et al.(2025)] Zion Hefty, Paul Horn, Dylan King, and Florian Pfender. Improving R(3, k) in just two bites. arXiv preprint arXiv:2510.19718, 2025. [Jiang et al.(2022)] Albert Q. Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzygóźdź, Piotr Miłoś, Yuhuai Wu, and Mateja Jamnik. Thor: Wielding hammers to integrate language models and automated theorem provers. In Advances in Neural Information Processing Systems, 2022. [Kontorovich(2025)] Alex Kontorovich. The shape of math to come. arXiv preprint arXiv:2510.15924, 2025.
Acknowledgement: We thank Alex Kontorovich for helpful conversations which improved an earlier draft of 6 We do take the position that the development of autoformalization should not wait until such infrastructure is “complete”; we believe that many hard papers can be autoformalized today, and that developing excellent systems for this task both provides real value and a stronger impetus for infrastructure development. 7 Kontorovich has discussed the problem of closing the loop from autoformalization to infrastructure-building under the name autocanonization [Kontorovich(2026)].
14
[Kontorovich(2026)] Alex Kontorovich. Interactions of AI with research math and formalization. Lecture at the “AI for Maths and Open Science” conference, Isaac Newton Institute, Cambridge; https://alexkontorovich. wordpress.com/2026/04/05/lecture-inter actions-of-ai-with-research-math-and -formalization-at-newton-insitute-cam bridge/, 2026. [Lamport(2002)] Leslie Lamport. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley, 2002.
(Auto)formalization is supposed to be easy
[Pegden(2026a)] Wesley Pegden. Trellis Lean formalization of Improving R(3, k) in just two bites (Hefty, Horn, King, and Pfender). Repository https://github.com/w pegden/twobites; formalization viewer https: //math.cmu.edu/˜wes/trellis/twobites-v iewer/, 2026. [Pegden(2026b)] Wesley Pegden. Trellis Lean formalization of Nearly tight exponents for off-diagonal Ramsey numbers (Bradač). Repository https://github.com/wpe gden/offdiagonal; formalization viewer https: //math.cmu.edu/˜wes/trellis/offdiagon al-viewer/, 2026. [Pegden(2026c)] Wesley Pegden. Trellis (source repository). https://github.com/wpegden/trellis, 2026. [Polu and Sutskever(2020)] Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393, 2020. [Szegedy(2020)] Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. In Intelligent Computer Mathematics, 2020. [Wu et al.(2022)] Yuhuai Wu, Albert Q. Jiang, Wenda Li, Markus N. Rabe, Charles Staats, Mateja Jamnik, and Christian Szegedy. Autoformalization with large language models. In Advances in Neural Information Processing Systems, 2022. [Yang et al.(2023)] Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J. Prenger, and Animashree Anandkumar. LeanDojo: Theorem proving with retrieval-augmented language models. In Advances in Neural Information Processing Systems, 2023. [Zheng et al.(2022)] Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: A cross-system benchmark for formal Olympiad-level mathematics. In International Conference on Learning Representations, 2022.
15