pith. sign in

arxiv: 2606.09674 · v1 · pith:B3PHPROMnew · submitted 2026-06-08 · 💻 cs.AI · cs.LO· math.CO

(Auto)formalization is supposed to be easy: Trellis process semantics for spelling out rigorous proofs

Wesley Pegden This is my paper

Pith reviewed 2026-06-27 16:27 UTC · model grok-4.3

classification 💻 cs.AI cs.LOmath.CO
keywords autoformalizationLean theorem proverLLM agentsprocess semanticsRamsey theoryformal verificationproof elaborationiterative refinement
0
0 comments X

The pith

A deterministically constrained workflow lets generalist LLM agents reliably turn natural language proofs into Lean formalizations.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper presents Trellis, a system that guides LLM agents through iterative refinement of natural language proofs into Lean code using a workflow that enforces the idea that rigorous proofs can always be elaborated further. This approach aims to achieve reliable autoformalization on a modest budget by relying on generalist agents rather than specialized training. The motivation comes from the common notion among mathematicians of what constitutes rigor. If successful, it suggests that the key to autoformalization lies in structuring the process rather than in the agents themselves. They demonstrate this with an end-to-end formalization of a recent Ramsey theory result.

Core claim

Trellis achieves reliable autoformalization on a modest budget and with generalist agents, with specialization coming from a meaning-of-rigor inspired workflow enforced by process semantics, as shown by an end-to-end Lean formalization of a recent Ramsey theory breakthrough.

What carries the argument

The deterministically constrained workflow based on process semantics, which enforces incremental progress by requiring routine elaboration of any part of a natural language proof into Lean.

If this is right

  • Complex mathematical results can be formalized in Lean without custom agent training or large-scale fine-tuning.
  • Autoformalization becomes feasible on modest computational budgets using only generalist LLM agents.
  • The workflow ensures incremental progress and reliable elaboration for end-to-end formalization of advanced theorems.
  • Specialization for formalization tasks arises from process design rather than model modification.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same workflow approach could extend to other proof assistants or formal systems beyond Lean.
  • Structured processes might improve reliability in other complex LLM agent tasks where incremental refinement matters.
  • Testing the system on additional recent mathematical breakthroughs would clarify its scalability across domains.

Load-bearing premise

That a deterministically constrained workflow based on process semantics can enforce incremental progress and reliable elaboration in complex Lean autoformalization tasks when using unmodified generalist LLM agents.

What would settle it

Applying the Trellis workflow to the recent Ramsey theory breakthrough and observing whether it produces a complete, verified Lean formalization or gets stuck on unresolvable errors despite the constraints.

Figures

Figures reproduced from arXiv: 2606.09674 by Wesley Pegden.

Figure 1
Figure 1. Figure 1: The human-protected core of one of the five targets ( [PITH_FULL_IMAGE:figures/full_fig_p005_1.png] view at source ↗
Figure 2
Figure 2. 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. 1 20 40 60 80 100 120 140 0 5, … view at source ↗
Figure 3
Figure 3. Figure 3: The natural-language proof corpus through the elab￾oration process. By the end of theorem stating the total LATEX proof words (green) already exceed 6,000—more than the tar￾get 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 obli￾gation ends supported by a valid Lean proof. T… view at source ↗
Figure 4
Figure 4. 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 … view at source ↗
Figure 5
Figure 5. 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 c… view at source ↗
Figure 7
Figure 7. Figure 7: Shallow-coarse progress in the run on the Bradac pa- ˇ per: how many of the 20 coarse milestones are fully shallow￾coarse-closed, by cycle. It rises monotonically to all 20; the shaded plateau (cycles 80–101) is a stall that tripped a Stuck￾MathAudit. cal work is completed. The deterministic checks above are run in an iso￾lated checker: a long-running, supervisor-owned server reached over a local unix sock… view at source ↗
read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 1 minor

Summary. The paper presents Trellis, an autoformalization system that uses LLM agents within a deterministically constrained workflow based on process semantics. The workflow is motivated by the notion that a rigorous proof is one that can be routinely elaborated in further detail, and it aims to enforce incremental progress and reliable elaboration of natural language proofs into Lean formalizations. Specialization arises from the workflow rather than task-specific agent training or fine-tuning. The central demonstration is an end-to-end Lean formalization of a recent Ramsey theory breakthrough, which is linked in the paper.

Significance. If the process semantics can be shown to enforce the claimed incremental progress and reliability with unmodified generalist agents, the approach would offer a practical route to autoformalization that avoids heavy specialization or large-scale training. The linked machine-checked Lean formalization of a recent Ramsey theory result constitutes a concrete, verifiable achievement that strengthens the paper's applicability claim.

major comments (2)
  1. [Abstract] Abstract: The central claim that the deterministically constrained workflow (rather than agent pre-training or unmentioned steering) produces reliable results rests on the existence of one linked Lean formalization. No description is given of the formal definition of the process semantics, the mechanisms for their mechanical enforcement, examples of agents proposing invalid steps that were rejected, or recovery from dead-ends.
  2. [Abstract] Abstract: No quantitative evidence is supplied to support 'reliable autoformalization on a modest budget,' such as token counts, iteration statistics, success rates across multiple tasks, or ablation runs that disable the process-semantics constraints while keeping the same generalist agents.
minor comments (1)
  1. [Abstract] The abstract introduces 'process semantics' without a brief definition or pointer to the section where the semantics are formalized.

Simulated Author's Rebuttal

2 responses · 1 unresolved

We thank the referee for their constructive comments, which highlight areas where the manuscript can be strengthened. We address each major comment below and outline our plans for revision.

read point-by-point responses

  1. Referee: Abstract: The central claim that the deterministically constrained workflow (rather than agent pre-training or unmentioned steering) produces reliable results rests on the existence of one linked Lean formalization. No description is given of the formal definition of the process semantics, the mechanisms for their mechanical enforcement, examples of agents proposing invalid steps that were rejected, or recovery from dead-ends.

    Authors: We agree that additional details are needed to support the central claim. The current manuscript motivates the use of process semantics but does not include the formal definition, enforcement mechanisms, or examples of invalid step rejections and dead-end recovery. We will revise the paper to include a formal definition of the process semantics, describe the mechanical enforcement in the workflow, and provide examples from the Ramsey theory case study. revision: yes

  2. Referee: Abstract: No quantitative evidence is supplied to support 'reliable autoformalization on a modest budget,' such as token counts, iteration statistics, success rates across multiple tasks, or ablation runs that disable the process-semantics constraints while keeping the same generalist agents.

    Authors: We agree that the paper lacks quantitative evidence beyond the single case study. We will add token counts and iteration statistics from the formalization process. However, success rates across multiple tasks and ablation runs were not performed. We will acknowledge this as a limitation and indicate that such evaluations are planned for future work, while maintaining that the linked Lean formalization provides concrete evidence of the approach's potential. revision: partial

standing simulated objections not resolved
  • We did not perform ablation runs or multi-task evaluations, so we cannot supply the requested comparative data or success rates at this time.

Circularity Check

0 steps flagged

No circularity; empirical demonstration stands independent of inputs

full rationale

The paper presents Trellis as a workflow system motivated by an external philosophical definition of rigor (elaborability of proofs) and supports its claims via a linked external Lean artifact. No equations, fitted parameters, predictions, or self-citations appear in the provided text that would reduce the central claim to its own inputs by construction. The workflow description and the Ramsey formalization are presented as separate elements, with no reduction of one to the other via definition or self-reference. This is the common case of a self-contained empirical report.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

No free parameters, axioms, or invented entities are identifiable from the abstract. The approach relies on existing LLM technology and the informal notion of rigor as elaborability, but supplies no new postulates or fitted quantities.

pith-pipeline@v0.9.1-grok · 5661 in / 1035 out tokens · 24480 ms · 2026-06-27T16:27:17.774656+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

14 extracted references · 2 linked inside Pith

  1. [1]

    The Lean mathematical library

    [The mathlib Community(2020)] The mathlib Community. The Lean mathematical library. InProceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs,

    2020

  2. [2]

    Nearly tight exponents for off-diagonal Ramsey numbers

    [Bradaˇc(2026)] Domagoj Brada ˇc. Nearly tight exponents for off-diagonal Ramsey numbers. arXiv preprint arXiv:2605.28793,

    Pith/arXiv arXiv 2026

  3. [3]

    The Lean Theorem Prover (System Description)

    [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). InAuto- mated Deduction - CADE-25,

    2015

  4. [4]

    Rabe, Talia Ringer, and Yuriy Brun

    [First et al.(2023)] Emily First, Markus N. Rabe, Talia Ringer, and Yuriy Brun. Baldur: Whole-proof generation and re- pair with large language models. InProceedings of the 31st ACM Joint European Software Engineering Confer- ence and Symposium on the Foundations of Software En- gineering,

    2023

  5. [5]

    ImprovingR(3, k)in just two bites

    [Hefty et al.(2025)] Zion Hefty, Paul Horn, Dylan King, and Florian Pfender. ImprovingR(3, k)in just two bites. arXiv preprint arXiv:2510.19718,

    arXiv 2025

  6. [6]

    Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzyg ´o´zd´z, Piotr Miło´s, Yuhuai Wu, and Mateja Jamnik

    [Jiang et al.(2022)] Albert Q. Jiang, Wenda Li, Szymon Tworkowski, Konrad Czechowski, Tomasz Odrzyg ´o´zd´z, Piotr Miło´s, Yuhuai Wu, and Mateja Jamnik. Thor: Wield- ing hammers to integrate language models and automated theorem provers. InAdvances in Neural Information Pro- cessing Systems,

    2022

  7. [7]

    The shape of math to come

    [Kontorovich(2025)] Alex Kontorovich. The shape of math to come. arXiv preprint arXiv:2510.15924,

    arXiv 2025

  8. [8]

    AI for Maths and Open Science

    [Kontorovich(2026)] Alex Kontorovich. Interactions of AI with research math and formalization. Lecture at the “AI for Maths and Open Science” conference, Isaac Newton In- stitute, Cambridge;https://alexkontorovich. wordpress.com/2026/04/05/lecture-inter actions- of- ai- with- research- math- and -formalization-at-newton-insitute-cam bridge/,

    2026

  9. [9]

    Addison-Wesley,

    [Lamport(2002)] Leslie Lamport.Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. Addison-Wesley,

    2002

  10. [10]

    Generative language modeling for automated theorem proving

    [Polu and Sutskever(2020)] Stanislas Polu and Ilya Sutskever. Generative language modeling for automated theorem proving. arXiv preprint arXiv:2009.03393,

    Pith/arXiv arXiv 2020

  11. [11]

    A promising path towards autoformalization and general artificial intelligence

    [Szegedy(2020)] Christian Szegedy. A promising path towards autoformalization and general artificial intelligence. InIn- telligent Computer Mathematics,

    2020

  12. [12]

    Jiang, Wenda Li, Markus N

    [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. InAdvances in Neural Information Processing Systems,

    2022

  13. [13]

    Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan J

    [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. Lean- Dojo: Theorem proving with retrieval-augmented lan- guage models. InAdvances in Neural Information Pro- cessing Systems,

    2023

  14. [14]

    miniF2F: A cross-system benchmark for formal Olympiad-level mathematics

    [Zheng et al.(2022)] Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. miniF2F: A cross-system benchmark for formal Olympiad-level mathematics. InInternational Conference on Learning Representations,

    2022