Multi-agent Autoformalization of Tensor Network Theory

Erickson Tjoa; J. Ignacio Cirac; Sirui Lu

REVIEW

Multi-agent Autoformalization of Tensor Network Theory

Sirui Lu, Erickson Tjoa, J. Ignacio Cirac

Quantum Physics · Submitted 8 Jul 2026 · 77 references

Pith's verdict: This is a real, machine-checked formalization of FT-MPS plus a documented multi-agent workflow; the main soft spot is that “autonomous” still means human intent review, which the authors already treat as the central finding.

T0 · AI review

How this review was made: An AI referee (grok-4.5) read the paper on July 10, 2026 and answered a fixed list of questions about it. T0 is the starting level every paper gets. The levels describe how deeply Pith has checked the paper, never the authors.

T0 AI review An AI read the paper and answered a fixed list of questions.
T1 Audit Automatic checks that the references and files the paper relies on exist and match.
T2 Compute The paper's code or calculations re-run with the same results.
T3 Formal statement The claims written out in a formal math language a computer can read.
T4 Proof Those claims proved, and the proof checked by computer.

How Pith checks papers →

· 2 major objections · 6 minor · Ask about this paper · The compiled record · Read the full review →

Challenge this review Comment (0) Read on arXiv ↗

Cite ▾

arXiv ID2607.07857 (version 1)

Pith IDYIW5RPHG, Pith's permanent record of this paper and its review

CitationErickson Tjoa, J. Ignacio Cirac, Sirui Lu. "Multi-agent Autoformalization of Tensor Network Theory." arXiv:2607.07857 (2026). https://pith.science/paper/YIW5RPHG

Cite this reviewBibTeX for Pith's review of this paper

Claim paper

Why Pith says this

Highlight any text to comment on it.

Editor's note

read the letter

The thing to know is that they actually finished a Lean formalization of the equal-case fundamental theorem of matrix-product states, with no core sorries, a public 12-chapter blueprint, and a sizable TNLean library (CP maps, quantum Perron–Frobenius, Wielandt, block separation, etc.) that Mathlib did not have. That is not vaporware methodology talk; the artifacts are the claim.

What is new is not FT-MPS itself—that is Pérez-García/Cirac standard—but the engineering stack: specialized agents, blueprint as the coordination medium, persistent memory, measured cost (~$20k API, ~$5.5k scaled to the FT-MPS core), and an unusually honest autopsy of intent failures. The agents also took a non-standard single-block route via Skolem–Noether, which is a nice side effect of leaning on Mathlib’s algebra rather than the usual spectral MPS path. The SPT cohomology invariant from injective symmetric MPS is a sensible first physical application, not a full phase classification.

They do well on the hard part of formalization: gap analysis (Jordan form, Burnside, Kadison–Schwarz, quantum PF, Brouwer), paper-to-Lean expansion numbers, and concrete wrong-but-compiling episodes (doubly stochastic “gauge,” asymptotic vs finite MPV comparison, oscillating repeated-block weights, D=0/N=0). Lean only checks the statement you wrote; they say that out loud and make it the main bottleneck. That is the right diagnosis.

Soft spots, in proportion: “autonomous” is qualified by six strategic blueprint reviews and human steering of intent. That does not sink the paper—it is the paper’s thesis—but anyone citing this as pure end-to-end AI formalization without human mathematical oversight would be misreading it. The full SPT classification (parent Hamiltonians, gapped paths) is left open, which is fine. Cost and model mix will age; the library and process notes will not.

This is for people who care about formal methods in mathematical physics, tensor networks, or multi-agent proof systems. The math of the formal core looks solid because the kernel checks it; the citation pattern is domain-normal. I would bring it to reading group, cite the library and the intent-failure case studies, and send it to peer review without hesitation.

Referee report

Significance

If the claims hold as stated, this is a substantial contribution at the intersection of formal methods, AI for science, and mathematical physics: a research-level theorem in tensor-network theory is machine-checked end-to-end, with open Lean libraries (CP maps, quantum Perron–Frobenius ingredients, Wielandt bound, canonical forms) that others can reuse, and an explicit SPT application. Strengths that should count in the assessment include Lean-kernel verification with no core sorries, a public blueprint with dependency graph and checkdecls-style links, honest gap analysis (Mathlib missing Jordan form, Burnside, Kadison–Schwarz, quantum PF, Brouwer) with documented workarounds, and transparent cost/orchestration artifacts. The methodological finding—that intent drift is the scaling bottleneck—is itself useful for the autoformalization community.

Major objections (2)

[Abstract; Introduction; Catching unintended formalizations] Abstract and opening claim that agents “orchestrated and executed the full formalization autonomously” sit in tension with the body (six blueprint review rounds; human supervisor sets and audits intent; primary arXiv sources supplied after an early autonomous attempt failed for multi-block FT-MPS). The central engineering claim remains defensible, but the abstract should state the same scope as the Discussion: agents handle tactical formalization under blueprint-mediated strategic human review. Without that alignment, readers will over-read “autonomous” relative to the documented process.
[Catching unintended formalizations; Method / End Matter; Supplementary Sec. E] The load-bearing soft point is already named by the authors: Lean checks the theorem as stated, not that it is the literature-intended theorem (doubly-stochastic gauge; asymptotic vs finite-N MPV equality; oscillating repeated-block weights ∑ μ_{j,q}^N). The paper reports six review rounds and repair, but does not give a reproducible criterion for when human review is “done” (e.g., checklist that hypotheses are no stronger than [28–30], finite-N comparison, D,N≥1). A short explicit review protocol or acceptance criteria in the Method/End Matter would make the weakest assumption auditable rather than anecdotal.

Minor objections (6)

[Theorem 1; Fig. 2; Supplementary Sec. B] Theorem 1 is stated for tensors already in CF; the reduction to CF (blocking, discarding off-diagonal triangular blocks, quantum Wielandt) is essential to the physical claim. A one-sentence pointer in the theorem statement or caption of Fig. 2 to the formalized reduction chain would help non-specialists.
[Abstract; Theorem 2; Physical application] Theorem 2 is correctly limited to a cohomological invariant from injective symmetric MPS, not the full 1D SPT classification (parent Hamiltonians, gapped paths). The Discussion already notes this; a matching caveat in the abstract’s “extends towards SPT” sentence would avoid overstatement.
[Introduction; Supplementary Sec. F] Cost figure ($20,206 full library; ~$5,548 scaled for FT-MPS by LOC) is useful but approximate. State explicitly that scaling by lines of code is a proxy, not a causal attribution, and that automated review agents outside the interactive runtime are excluded.
[The fundamental theorem and its formalization; Fig. 1] Notation: Ai vs A_i and Γ_L vs spanning condition are discussed in Fig. 1; ensure the main-text definition of “normal” and “CF” matches the blueprint’s formal hypotheses (spectral radius 1, unique peripheral eigenvalue) so auditors do not need the HTML graph for the statement alone.
[Abstract] Minor prose: “\nChapters{}-chapter” in the abstract is a macro placeholder; fix to “12-chapter” for the journal version. Check arXiv id formatting and consistent spelling of “autoformalization.”
[Introduction; Discussion and outlook] Cite or briefly contrast related concurrent Lean/QI efforts (e.g., generalized quantum Stein’s lemma formalizations, PhysLib, MerLean) in one paragraph so the novelty claim is positioned against the nearest neighbors already mentioned in the bibliography.

How Pith checks papers → · Full audit of this paper →

The paper

The paper claims

Specialized LLM agents, guided by a shared blueprint and sparse human review, fully formalized the fundamental theorem of matrix-product states in Lean.

The reading

The paper shows that a team of specialized language-model agents can carry out a research-level formalization in theoretical physics: the equal-case fundamental theorem of matrix-product states, checked end-to-end in Lean 4 with no unfinished steps in the core argument. Agents scout libraries, write proofs, simplify code, and keep a human-readable mathematical blueprint aligned with the formal declarations, while a human supervisor only sets and audits mathematical intent. Along the way they built large tensor-network and quantum-information libraries that were missing from Mathlib and derived a cohomological invariant for one-dimensional symmetry-protected topological phases from injective symmetric MPS. The demonstration is offered as evidence that the hard remaining problem is not closing individual lemmas but keeping formal statements faithful to the intended physics theorems.

What carries the argument

The blueprint-plus-agents architecture: a human-readable, dependency-tagged mathematical blueprint that links literature statements to Lean declarations, together with specialized agents (orchestrator, scout, prover, simplifier, blueprint synchronizer, reviewer) and persistent memory that split the work into bounded sessions while the human only corrects strategic intent drift.

Extended reading notes

Core claim

A multi-agent LLM workflow, coordinated by a structured mathematical blueprint and periodic human review of intent, can autonomously orchestrate and complete the research-level Lean formalization of the equal-case fundamental theorem of matrix-product states, producing extensive new tensor-network and quantum-information libraries and a first formal cohomological SPT invariant, while identifying enforcement of mathematical intent as the central bottleneck.

Load-bearing premise

That a few rounds of human strategic review of the blueprint are enough to catch when agents prove a weaker or wrong version of a theorem before large stacks of later lemmas are built on that wrong statement.

Editorial extensions

If this is right

The same agent-and-blueprint pattern can target other tensor-network results already listed as natural extensions: boundaries, parent Hamiltonians, matrix-product operators, and renormalization fixed points.
The released TNLean infrastructure and technique notes give a reusable base for formalizing further quantum-information and many-body statements that previously lacked Mathlib support.
When agents choose non-standard routes (for example single-block FT-MPS via Skolem–Noether), the formal library can record alternative proof strategies that the physics literature does not use.
The cohomological SPT invariant extracted from injective symmetric MPS becomes a formal starting point for completing the one-dimensional bosonic SPT classification inside Lean.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

Intent-enforcement cost will dominate scale more than raw proof-search cost, so future systems need better automated checks that a formal statement matches the literature claim, not only that Lean accepts it.
Blueprint-guided multi-agent formalization may transfer to other areas where physics results sit outside pure mathematical physics and therefore require filling informal gaps into checkable statements.
Persistent memory of rejected routes and false statements could become a shared resource across formalization projects, reducing repeated dead ends.

Original abstract

We build a team of specialized large language-model agents and present an agent-driven workflow for research-level formalization in theoretical physics, with the autoformalization of the fundamental theorem of matrix-product states as a demonstration. The agents, coordinated through a structured mathematical blueprint and periodic human review, orchestrated and executed the full formalization autonomously. For some statements, the agents were able to explore new proof routes that are not part of the standard literature. Along the way the agents produced extensive tensor-network and quantum-information libraries not previously available in Mathlib, Lean's mathematical library. As a physical application, the formalization also extends towards symmetry-protected topological phases in one dimension. We find that the main bottleneck in large-scale autoformalization is enforcing mathematical intent and we provide a detailed study of the full process and various subtleties involved. We release the codebase as the library \href{https://github.com/LionSR/TNLean}{TNLean}, together with a \nChapters{}-chapter \href{https://lionsr.github.io/TNLean/blueprint/}{blueprint} of the formalization effort.

The compiled record

The paper's own sentences, arranged, kept beside the review and separate from it. Each label is drawn from a closed vocabulary; the number beside it is the probability the classifier gave that label. Numbers in the tables are the authors', checked by code. No sentence in this record was written by a model.

Compiled by classifier-1.13.0 via TypeSafe API, question bank abstract-p1-20260923, 2026-09-23: 1 request, 5,705 input tokens.

What the abstract itself states, as probabilities: claims first 0.10 · states limitation 0.92 · human participants 0.42 · controlled comparison 0.02 · randomized assignment 0.01 · states quantitative result 0.13 · compares with prior results 0.18 · mentions code or data availability 0.98.

The abstract, sentence by sentence

arXiv listing abstract v1. Results and the main claim are underlined; show every role.

We build a team of specialized large language-model agents and present an agent-driven workflow for research-level formalization in theoretical physics, with the autoformalization of the fundamental theorem of matrix-product states as a demonstration. The agents, coordinated through a structured mathematical blueprint and periodic human review, orchestrated and executed the full formalization autonomously. For some statements, the agents were able to explore new proof routes that are not part of the standard literature. Along the way the agents produced extensive tensor-network and quantum-information libraries not previously available in Mathlib, Lean's mathematical library. As a physical application, the formalization also extends towards symmetry-protected topological phases in one dimension. We find that the main bottleneck in large-scale autoformalization is enforcing mathematical intent and we provide a detailed study of the full process and various subtleties involved. We release the codebase as the library \href{https://github.com/LionSR/TNLean}{TNLean}, together with a \nChapters{}-chapter \href{https://lionsr.github.io/TNLean/blueprint/}{blueprint} of the formalization effort.

background contribution method result interpretation main claim

What the classifier reports for each sentence. The number is the probability it gave the label.
#	sentence	role	the authors' own work	states the main conclusion	strength
s0	We build a team of specialized large language-model agents and present an agent-driven workflow for research-level formalization in theoretical physics, with the autoformalization of the fundamental theorem of matrix-product states as a demonstration.	contribution 0.99	0.96	0.16	asserted 1.00
s1	The agents, coordinated through a structured mathematical blueprint and periodic human review, orchestrated and executed the full formalization autonomously.	method 0.90	0.81	0.09	asserted 1.00
s2	For some statements, the agents were able to explore new proof routes that are not part of the standard literature.	result 0.89	0.87	0.06	asserted 0.70
s3	Along the way the agents produced extensive tensor-network and quantum-information libraries not previously available in Mathlib, Lean's mathematical library.	contribution 0.62	0.91	0.04	asserted 1.00
s4	As a physical application, the formalization also extends towards symmetry-protected topological phases in one dimension.	contribution 0.62	0.88	0.04	asserted 0.99
s5	We find that the main bottleneck in large-scale autoformalization is enforcing mathematical intent and we provide a detailed study of the full process and various subtleties involved.	result 0.74	0.95	0.81	asserted 1.00
s6	We release the codebase as the library \href{https://github.com/LionSR/TNLean}{TNLean}, together with a \nChapters{}-chapter \href{https://lionsr.github.io/TNLean/blueprint/}{blueprint} of the formalization effort.	contribution 0.99	0.95	0.05	asserted 0.99

What kind of paper the classifier reports this is: method or tool 1.00 · evidence from proof or derivation 0.88.

What was examined, and what was not

sources read

arXiv listing abstract v1

not examined

full text
figures and tables
references and citing sentences
relations to other papers

levels run

P abstract

not run

S sections
T body sentences
C citations
R cross-paper relations

Every quoted sentence on this record is the authors'. Every label is from Pith's closed vocabulary, with the probability shown beside it. Every number in the measurements table is the authors', checked by code. Record as JSON

Figures

**Figure 1.** FIG. 1. Maintaining consistency across the literature, Lean, and the blueprint. A theorem stated in several sources under different

**Figure 2.** FIG. 2. Blocking in tensor networks. Given an MPS ten

**Figure 3.** FIG. 3. From the fundamental theorem to the classification

**Figure 4.** FIG. 4. System architecture and orchestration patterns.

**Figure 5.** FIG. 5. Token usage by agent role, each bar broken down

**Figure 6.** FIG. 6. Model usage over the project. Newer model releases

Figures reproduced from arXiv:2607.07857 by the authors.

References

Works cited (77)

[1]

Review-repair cycles Review and repair phases in alternating fashion. A review agent, typically the automated reviewer or leanBlueprint, identifies discrepancies: paper-vs-Lean mismatches, missing hypotheses, style violations, or blueprint drift. Repair agents address the identified issues, and the review is repeated to verify the fixes and catch regressi...

View on Pith
[2]

Proof strategy divergences The injective-case route via the Skolem–Noether theorem, described in the main text and reproduced in Sec. G, is one example of a divergence between the formal proof and the standard MPS literature; the divergences below cover the remaining cases. When autoformalization is carried out across different resources with different co...

View on Pith
[3]

Formal correctness vs. mathematical intent As discussed in the main text, the system can produce formally correct proofs of statements that are weaker or more special than the intended theorem. Lean checks the theorem as stated; by type checking alone, it does not verify that the statement matches the result intended from the literature. This occurred whe...

View on Pith
[4]

Paper-to-Lean expansion A persistent feature of the formalization is that short arguments in the paper expand into longer chains of interme- diate Lean lemmas. The expansion is uneven: algebraic arguments usually grow by a small factor, while spectral arguments requiring new supporting lemmas can grow by an order of magnitude. Several representative examp...

View on Pith
[5]

Mathlib gaps and workarounds The formalization encountered five gaps in the Mathlib library, each requiring a custom replacement (Table S4). TABLE S4. Mathlib gaps encountered and their replacements. Missing from Mathlib Replacement used Jordan normal form Generalized eigenspaces and an invertible/nilpotent decomposition Burnside’s theorem for matrix alge...

View on Pith 2026
[6]

AgentleanOrchestrator: task decomposition and dispatch The orchestrator plans the formalization, decomposes it into bounded tasks, and dispatches them to the specialized roles below. name: leanOrchestrator description: Lean 4 project orchestrator—coordinates formalization, delegates to specialized Lean agents, and manages proof development workflow. setti...

View on Pith
[7]

Agentlean: proof writing The proof writer develops formal proofs through iterative refinement, closing unfinished steps and repairing broken proof chains. name: lean description: Lean 4 proof assistant with VS Code integration and CLI fallback. settings: agentCategory: toolUse tools: - todo_write - lean_diagnostics - lean_file - lean_project - lean_inspec...

View on Pith
[8]

AgentleanSearch: Mathlib scouting and research The library scout locates existing lemmas in Mathlib and the wider literature, its purpose being to prevent duplicate formalization work. name: leanSearch description: Lean 4 and Mathlib research assistant—finds lemmas, explores APIs, and answers formalization questions. settings: agentCategory: toolUse tools...

View on Pith
[9]

**lean_loogle** —Search Mathlib by type signature or name pattern. This is your first tool for " does this lemma exist?" - Type signature search:`"(?a :N)→?a + 0 = ?a"`finds`Nat.add_zero` - Name pattern search:`"List.map"`finds all`List.map`lemmas - Subexpression search:`"_ * (_ ^ _)"`finds lemmas with that shape - Conclusion search:`"|- tsum _ = _ * tsum...

View on Pith
[10]

**grep on .lake/packages/mathlib/** —Search Mathlib source directly when it's available (after` lake build`or`lake exe cache get`): - Exact identifier lookup:`grep "theorem add_comm" .lake/packages/mathlib/Mathlib/` - Find all lemmas about a concept:`grep "tsum" .lake/packages/mathlib/Mathlib/Topology/Algebra/ InfiniteSum/` - Find how something is used:`g...

View on Pith
[11]

**glob on .lake/packages/mathlib/** —Find relevant Mathlib files by path: -`glob ".lake/packages/mathlib/Mathlib/ **/*Matrix*.lean"`finds all matrix-related files -`glob ".lake/packages/mathlib/Mathlib/Topology/ **/*.lean"`lists the topology hierarchy - Useful for understanding Mathlib's module structure and finding the right import

View on Pith
[12]

**web_search + web_fetch** —Search beyond the local project: - Lean 4 documentation and release notes - Lean Zulip archive (https://leanprover.zulipchat.com)—the primary community Q&A - Mathlib documentation (https://leanprover-community.github.io/mathlib4_docs/) - Lean 4 source and GitHub issues - Blog posts and tutorials on Lean formalization techniques

View on Pith
[13]

**arxiv_search + arxiv_metadata + download_arxiv_source** —Find and retrieve academic papers: - arxiv_search: Find papers by topic, author, or keyword (e.g., "Lean 4 formalization", "Mathlib category theory") - arxiv_metadata: Get full metadata (abstract, authors, dates) for a known arXiv ID - download_arxiv_source: Download the LaTeX source of a paper fo...

View on Pith
[14]

**lean_inspect** —Examine types and proof states in the user's own code: 33 -`hover`on an identifier to see its full type signature and docstring -`goal`inside a tactic block to see what remains to be proved -`term_goal`to see the expected type at a position

View on Pith
[15]

**lean_diagnostics** —Check what errors/warnings exist in a file before suggesting fixes ## Research Workflows ### "Does this lemma exist in Mathlib?"

View on Pith
[16]

Search lean_loogle with the type signature (try multiple formulations—swap args, use`↔`vs`→ `)

View on Pith
[17]

If Loogle finds nothing, grep .lake/packages/mathlib/ for key identifiers in the statement

View on Pith
[18]

If grep finds nothing, search the Mathlib docs website with web_search

View on Pith
[19]

If truly missing, check Lean Zulip for discussions about it—someone may have a PR in progress

View on Pith
[20]

Report what you found. If it doesn't exist, suggest: (a) the most general statement to formalize, ( b) which Mathlib file it would belong in, (c) what the canonical name would be per naming conventions ### "How do I formalize X?"

View on Pith
[21]

Search Mathlib for existing formalizations of similar or related concepts

View on Pith
[22]

Find the right algebraic hierarchy—e.g., for a ring property, is it at`CommRing`,`Ring`, or` Semiring`level?

View on Pith
[23]

Read existing Mathlib files in that area to understand conventions (import patterns, naming, proof style)

View on Pith
[24]

Search Lean Zulip for formalization discussions about X

View on Pith
[25]

Propose a formalization plan: definitions, key lemmas, and which Mathlib files to import ### "What tactic should I use for this goal?"

View on Pith
[26]

Use lean_inspect to see the exact goal state

View on Pith
[27]

Identify the goal structure: equational? ordering? arithmetic? set membership? decidable?

View on Pith
[28]

Recommend tactics from Mathlib's tactic library: - **Closing tactics**:`simp`,`omega`,`decide`,`norm_num`,`ring`,`linarith`,`positivity`,` field_simp`,`norm_cast`,`push_cast`,`Abel`,`group` - **Rewriting**:`rw`,`simp only`,`conv`,`ring_nf`,`push_neg` - **Case analysis**:`rcases`,`obtain`,`match`,`by_cases`,`by_contra` - **Construction**:`exact`,`refine`,`...

View on Pith
[29]

If stuck, search for proofs of similar goals in Mathlib source for patterns ### "Find the paper / proof for this result"

View on Pith
[30]

Use arxiv_search to find papers about the topic (try author names, theorem names, keywords from the statement)

View on Pith
[31]

Use arxiv_metadata to check abstracts and confirm relevance

View on Pith
[32]

Use download_arxiv_source to get the LaTeX—read the actual proof strategy, not just the abstract

View on Pith
[33]

Cross-reference with Mathlib: search for the paper's arXiv ID in Mathlib docstrings (`grep "arXiv" . lake/packages/mathlib/`) to see if it's already been formalized

View on Pith
[34]

Summarize: the paper's approach, which results are formalized vs not, and how the informal proof maps to potential Lean tactics ### "What's the API for X?"

View on Pith
[35]

Use lean_loogle to find all lemmas mentioning X

View on Pith
[36]

Use glob to find the Mathlib file(s) where X is defined

View on Pith
[37]

Read those files to see the full API: definition, simp lemmas, ext lemmas, coercions, instances

View on Pith
[38]

Summarize: what's defined, what the key lemmas are, what instances exist, and the import path ## Mathlib Navigation Knowledge Key module paths to know: -`Mathlib.Algebra. *`—algebraic structures and operations -`Mathlib.Order. *`—order theory, lattices, filters -`Mathlib.Topology. *`—topological spaces, continuity, limits -`Mathlib.Analysis. *`—real/compl...

View on Pith
[39]

AgentleanSimplifier: proof simplification and style The simplifier refactors proofs toward the readability, generality, and naming conventions of the Mathlib library while preserving every statement. name: leanSimplifier description: Simplifies Lean 4 proofs and code to Mathlib-quality standards—clear, general, and ready to upstream. settings: agentCatego...

View on Pith
[40]

**Preserve Correctness**: Never change what a proof proves or what a definition computes—only how it expresses it. All theorem statements, instances, and computed values must remain identical. Use lean_diagnostics after every edit to confirm zero errors

View on Pith
[41]

**Enforce Mathlib Style**: - **Line length**: 100 characters max. Break long lines at operators, after`:=`, or before`by` - **Indentation**: 2 spaces. Continuation lines indented 2 more. Tactic blocks indented under`by` - **Declarations**: Use`theorem`for`Prop`-valued results,`def`for data,`lemma`for minor results used in proofs. Use`noncomputable`only wh...

View on Pith
[42]

**Follow Mathlib Naming Conventions**: This is critical for discoverability and upstreaming: - Theorem names describe the conclusion:`add_comm`,`mul_left_cancel`,`Nat.succ_le_iff` - Prefix with type when not in a namespace:`List.map_map`,`Finset.sum_add_sum` - Use these naming atoms consistently: - Operations:`add`,`mul`,`sub`,`div`,`neg`,`inv`,`pow`,`suc...

View on Pith
[43]

**Maximize Generality**: Mathlib values maximally general statements: - Use the weakest typeclass that suffices:`Monoid`over`Group`if the proof doesn't use`inv`,` AddCommGroup`over`ModuleZ`if scalar mul isn't needed - Use`variable`blocks with typeclass assumptions at the section level, not repeated on each declaration - Factor type-specific lemmas into ty...

View on Pith
[44]

**Simplify Tactic Proofs**: Replace verbose tactic sequences with clean, reviewable proofs: - Use`simp`with explicit lemma lists (`simp [h1, h2]`)—avoid bare`simp`(fragile, hard to review).`simp only [...]`is preferred for upstreaming as it pins the simp set - Use`omega`for linear arithmetic over`N`and`Z`instead of manual chains - Use`decide`for small dec...

View on Pith
[45]

**Use Idiomatic Lean 4 / Mathlib Patterns**: - Prefer`calc`blocks for equational chains—they show proof structure clearly - Use anonymous constructor`⟨a, b⟩`when the expected type is unambiguous - Use`fun x => ...`(not`λ`), dot notation (`h.symm`,`h.mp`), cdot (`·`) - Prefer`match`over`if ... then ... else`on inductive types - Use`where`for substantial au...

View on Pith
[46]

**Clean Up Structure and Organization**: - Remove duplicate`import`statements; sort imports alphabetically - Delete commented-out proofs,`sorry`-ed stubs, dead code,`#check`/`#eval`leftovers - Merge adjacent`namespace`/`section`blocks for the same namespace - Remove unnecessary explicit universe annotations and redundant type ascriptions - Collapse trivia...

View on Pith
[47]

**Remove Duplication via Generalization**: - Near-identical lemmas for different types→one generic lemma with typeclass constraints - Same proof for both directions of`Iff`→`Iff.intro`with shared reasoning, or`constructor <;> intro h <;> tactic` - Parallel multiplicative/additive lemmas→`@[to_additive]` - Repeated`simp`configurations→factor into a custom`...

View on Pith
[48]

**Leverage Mathlib—Don't Reinvent **: - Use lean_loogle to search by type signature *before* keeping any hand-written lemma - Search`.lake/packages/mathlib/`with grep for existing proofs - Common reinventions: basic algebra (`add_comm`,`mul_assoc`), order theory (`le_antisymm`,` lt_iff_le_not_le`), set operations (`Set.mem_union`,`Set.inter_comm`), finset...

View on Pith
[49]

**Informal–Formal Consistency**: Projects often pair Lean files with informal LaTeX notes (papers, blueprints, documentation). When both exist, check consistency: - **Statement alignment**: Verify that formal theorem statements match the informal claims in the LaTeX. Flag mismatches—a formal`≤`where the paper says`<`, a missing hypothesis, a different bou...

View on Pith
[50]

**Linting—The Upstream Gate **: 37 - All code should pass Mathlib's`#lint`checks. The main linters to satisfy: -`unusedArguments`: no unused hypotheses in theorem statements -`simpNF`: simp lemmas in normal form (LHS not already simplifiable) -`docBlame`: public declarations have docstrings -`dupNamespace`: no`Foo.Foo.bar`stuttering -`unusedHavesSuffices`...

View on Pith
[51]

**Maintain Balance**: Avoid over-simplification that could: - Obscure proof structure that aids mathematical understanding - Remove comments that explain mathematical insight or proof strategy (but do remove noise comments like`-- obvious`) - Merge proofs that handle genuinely different mathematical cases - Replace a readable`calc`with an opaque`simp`or`d...

View on Pith
[52]

**Focus Scope**: Only simplify code the user points to, unless explicitly asked to review broader scope. Read files before editing. Prefer edit_file for targeted modifications. Your refinement process:

View on Pith
[53]

Survey the target Lean files with glob and grep to understand project structure, imports, and dependencies

View on Pith
[54]

Read files fully before making any changes—understand the mathematical context

View on Pith
[55]

Use lean_diagnostics to check current state (errors, warnings, lint issues) before starting

View on Pith
[56]

Plan changes with todo_write, ordered: naming/style fixes→docstrings→generalization→proof simplification→deduplication

View on Pith
[57]

Apply one logical simplification per edit

View on Pith
[58]

After each edit, use lean_diagnostics to verify zero new errors—Lean's type checker is the ground truth

View on Pith
[59]

If lean_diagnostics reports errors after an edit, revert immediately and try a different approach

View on Pith
[60]

Use lean_inspect (goal state) to understand tactic proof states when simplifying complex proofs

View on Pith
[61]

Use lean_loogle and grep on .lake/packages/mathlib/ to find existing lemmas before keeping hand- written ones

View on Pith
[62]

After all changes, do a final lean_diagnostics pass to confirm clean state userRequest: | {{ INSTRUCTION }}

View on Pith
[63]

AgentleanBlueprint: blueprint authoring and synchronization The blueprint synchronizer writes and maintains the mathematical blueprint, keeping its prose and dependency graph in step with the Lean code. name: leanBlueprint description: Creates and maintains LeanBlueprint documents following Patrick Massot's plasTeX plugin ( https://github.com/PatrickMasso...

View on Pith
[64]

Survey the Lean project first. Use glob and grep to find .lean files, read_file to examine definitions and theorems, lean_inspect for type signatures. Understand the mathematical structure before writing anything. 1a. MANDATORY: if there is no`blueprint/`directory, stop and run`leanblueprint new`from the Lean project root before writing any`.tex`. This is...

View on Pith
[65]

Design the dependency DAG. Start from the main theorem(s), work backward. Each node should be one well-defined mathematical fact—not so large it takes weeks, not so small it clutters the graph. Make dependencies explicit and accurate

View on Pith
[66]

Write the content. Statements must be mathematically precise and written in standard mathematical notation—translate all Lean identifiers and type signatures into conventional symbols and prose (see NOTATION TRANSLATION above). Proof sketches should outline the strategy clearly enough for a formalizer to follow. Use \lean{} with the actual qualified Lean ...

View on Pith
[67]

Before writing any blueprint entry, search for existing formalizations and literature: - lean_loogle for type signature search in Mathlib - grep on .lake/packages/mathlib/ for identifier lookup - web_search for Zulip discussions and Mathlib docs - arxiv_search + download_arxiv_source when working from a paper - crossref_search + crossref_doi for published...

View on Pith
[68]

When building a blueprint from a paper: download the LaTeX source, identify all numbered results, trace which results cite which in their proofs, map each to Lean declarations if they exist, then generate the skeleton. SYNCING EXISTING BLUEPRINTS This is equally important as writing. When the Lean codebase evolves, the blueprint can drift out of sync. You...

View on Pith
[69]

Read the existing blueprint .tex files. Parse out every \lean{} reference, every \leanok, every \ uses{} dependency

View on Pith
[70]

Check each \lean{DeclName} against the Lean project. Use grep to verify the declaration exists. If it was renamed or deleted, update or remove the \lean{} reference. If a new declaration was added that corresponds to a blueprint item, add \lean{}

View on Pith
[71]

Check each \leanok. Use lean_diagnostics and lean_inspect to confirm the declaration compiles without sorry. If a proof was reverted to sorry, remove \leanok. If a previously unformalized item now has a clean proof, add \leanok

View on Pith
[72]

Check statement consistency. Use lean_inspect hover to get the Lean type signature and compare it to the LaTeX statement. Translate the Lean type into standard mathematical notation before comparing— the LaTeX statement should never mirror Lean syntax. Watch for: changed hypotheses, swapped quantifier order, different bounds (< vs <=), renamed variables, ...

View on Pith
[73]

Check \uses{} accuracy. When Lean declarations change their dependencies (using different lemmas, importing different modules), the blueprint \uses{} should reflect this. Spurious dependencies hide parallelism; missing ones produce a wrong graph

View on Pith
[74]

Look for new Lean declarations that have no blueprint entry. Use glob/grep to find theorems and definitions in the Lean source, then check whether each appears in the blueprint. For significant results missing from the blueprint, draft new entries

View on Pith
[75]

Look for blueprint entries with no Lean counterpart. These might be planned items (fine, leave them ), or they might reference declarations that were refactored away (update or remove)

View on Pith
[76]

Run leanblueprint checkdecls when available to verify all \lean{} references resolve

View on Pith
[77]

Fact-check the mathematical content. The blueprint is the human-readable reference for the project, so it must be mathematically correct independent of the Lean code. - Verify that stated hypotheses are sufficient. If a lemma claims "for all groups" but the proof uses commutativity, the statement needs a commutativity hypothesis. - Check that bounds, ineq...

View on Pith

Forward citations

Cited by 7 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score. Full citation record

Long-horizon autoformalization of a core theorem underlying MIP* = RE
quant-ph 2026-09 accept novelty 9.0 of 10 full

AI agents under human supervision generated a verified Lean 4 proof of the quantum soundness of the classical low individual-degree test, correcting errors in the published proof and establishing a route to affordable...
Higher tensor network states in two spatial dimensions: fundamental theorem for open boundary conditions
cond-mat.str-el 2026-11 accept novelty 8.0 of 10

A fundamental theorem for categorified tensor network states in two dimensions shows that two representations generating the same states are equivalent as module categories, generalizing known results to encompass ric...
Bridging Gaps with Tensor Networks: From the Haldane Gap and Beyond
quant-ph 2026-11 accept novelty 7.0 of 10 partial

A tensor-network reinterpretation and Lean 4 formalization of the AI-assisted Haldane gap proof yields sharper bounds, broader theorems for eight spin chains, and a reusable formal verification framework.
Classical and Quantum Simulation of All-to-All Quantum Dynamics in Logarithmic Space
quant-ph 2026-09 accept novelty 7.0 of 10

All-to-all spin dynamics (Dicke, Hopfield, and short-time SK models) can be simulated in logarithmic quantum space, with evidence that classical algorithms at matching resources would imply BQL subseteq SC.
Numina Fuse: Interactive Autoformalization in Lean 4
cs.AI 2026-10 conditional novelty 6.0 of 10

Numina Fuse is a system for interactive autoformalization in Lean4 that evolved from a hardcoded pipeline to an agent orchestrator, tested on the Kakeya conjecture and a prover cost study.

Show 2 more citing papers

Jianmu-Q: Bridging Quantum Field Theory and Quantum Hardware with AI Agents
hep-lat 2026-10 conditional novelty 6.0 of 10

A multi-agent AI framework converts QFT Lagrangians into validated quantum circuits, demonstrated on NJL, Schwinger, and Z2 gauge-theory benchmarks with hardware runs on IBM devices.
AxQM: A Textbook-Scale Benchmark for Formal Proof Synthesis in a Library of Finite-Dimensional Quantum Mechanics
quant-ph 2026-09 accept novelty 6.0 of 10

AxQM is a Lean benchmark with 1,019 proof-synthesis tasks covering 479 items from Nielsen and Chuang, making it the largest physics formalization benchmark by factor of four.

How the literature uses it

What this paper does with the arXiv papers it cites

Each citing sentence is taken from the citing paper's LaTeX source and typed by Pith's classifier. A label appears at probability 0.8 or more (0.95 for support), a contest at 0.7 or more; the quoted words are the citing authors'. How each label was checked · JSON

What it cites · 13 sentences without a confident label

Cites as background 4 papers

[equation] Eq. [ref] is not normalized as they are also relevant for studying matrix-product operators (see, e.g., [ref] ), thus they are also called matrix-product vectors (MPVs) [ref] .

Nilpotence theorems via homological residue fields · Introduction · 0.83
They have certified results from the four-color theorem [ref] to the Kepler conjecture [ref] , and AI systems can now find Lean 4 proofs automatically for many mathematical targets [ref] .

Kimina-Prover Preview: Towards Large Formal Reasoning Models with Reinforcement Learning · Introduction · 0.80
They have certified results from the four-color theorem [ref] to the Kepler conjecture [ref] , and AI systems can now find Lean 4 proofs automatically for many mathematical targets [ref] .

DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition · Introduction · 0.80

Discussion

Disagree with the review, or know something it missed? Leave a comment, highlight any passage above to comment on it, or challenge this review formally.

[1] [1]

Review-repair cycles Review and repair phases in alternating fashion. A review agent, typically the automated reviewer or leanBlueprint, identifies discrepancies: paper-vs-Lean mismatches, missing hypotheses, style violations, or blueprint drift. Repair agents address the identified issues, and the review is repeated to verify the fixes and catch regressi...

View on Pith

[2] [2]

Proof strategy divergences The injective-case route via the Skolem–Noether theorem, described in the main text and reproduced in Sec. G, is one example of a divergence between the formal proof and the standard MPS literature; the divergences below cover the remaining cases. When autoformalization is carried out across different resources with different co...

View on Pith

[3] [3]

Formal correctness vs. mathematical intent As discussed in the main text, the system can produce formally correct proofs of statements that are weaker or more special than the intended theorem. Lean checks the theorem as stated; by type checking alone, it does not verify that the statement matches the result intended from the literature. This occurred whe...

View on Pith

[4] [4]

Paper-to-Lean expansion A persistent feature of the formalization is that short arguments in the paper expand into longer chains of interme- diate Lean lemmas. The expansion is uneven: algebraic arguments usually grow by a small factor, while spectral arguments requiring new supporting lemmas can grow by an order of magnitude. Several representative examp...

View on Pith

[5] [5]

Mathlib gaps and workarounds The formalization encountered five gaps in the Mathlib library, each requiring a custom replacement (Table S4). TABLE S4. Mathlib gaps encountered and their replacements. Missing from Mathlib Replacement used Jordan normal form Generalized eigenspaces and an invertible/nilpotent decomposition Burnside’s theorem for matrix alge...

View on Pith 2026

[6] [6]

AgentleanOrchestrator: task decomposition and dispatch The orchestrator plans the formalization, decomposes it into bounded tasks, and dispatches them to the specialized roles below. name: leanOrchestrator description: Lean 4 project orchestrator—coordinates formalization, delegates to specialized Lean agents, and manages proof development workflow. setti...

View on Pith

[7] [7]

Agentlean: proof writing The proof writer develops formal proofs through iterative refinement, closing unfinished steps and repairing broken proof chains. name: lean description: Lean 4 proof assistant with VS Code integration and CLI fallback. settings: agentCategory: toolUse tools: - todo_write - lean_diagnostics - lean_file - lean_project - lean_inspec...

View on Pith

[8] [8]

AgentleanSearch: Mathlib scouting and research The library scout locates existing lemmas in Mathlib and the wider literature, its purpose being to prevent duplicate formalization work. name: leanSearch description: Lean 4 and Mathlib research assistant—finds lemmas, explores APIs, and answers formalization questions. settings: agentCategory: toolUse tools...

View on Pith

[9] [9]

**lean_loogle** —Search Mathlib by type signature or name pattern. This is your first tool for " does this lemma exist?" - Type signature search:`"(?a :N)→?a + 0 = ?a"`finds`Nat.add_zero` - Name pattern search:`"List.map"`finds all`List.map`lemmas - Subexpression search:`"_ * (_ ^ _)"`finds lemmas with that shape - Conclusion search:`"|- tsum _ = _ * tsum...

View on Pith

[10] [10]

**grep on .lake/packages/mathlib/** —Search Mathlib source directly when it's available (after` lake build`or`lake exe cache get`): - Exact identifier lookup:`grep "theorem add_comm" .lake/packages/mathlib/Mathlib/` - Find all lemmas about a concept:`grep "tsum" .lake/packages/mathlib/Mathlib/Topology/Algebra/ InfiniteSum/` - Find how something is used:`g...

View on Pith

[11] [11]

**glob on .lake/packages/mathlib/** —Find relevant Mathlib files by path: -`glob ".lake/packages/mathlib/Mathlib/ **/*Matrix*.lean"`finds all matrix-related files -`glob ".lake/packages/mathlib/Mathlib/Topology/ **/*.lean"`lists the topology hierarchy - Useful for understanding Mathlib's module structure and finding the right import

View on Pith

[12] [12]

**web_search + web_fetch** —Search beyond the local project: - Lean 4 documentation and release notes - Lean Zulip archive (https://leanprover.zulipchat.com)—the primary community Q&A - Mathlib documentation (https://leanprover-community.github.io/mathlib4_docs/) - Lean 4 source and GitHub issues - Blog posts and tutorials on Lean formalization techniques

View on Pith

[13] [13]

**arxiv_search + arxiv_metadata + download_arxiv_source** —Find and retrieve academic papers: - arxiv_search: Find papers by topic, author, or keyword (e.g., "Lean 4 formalization", "Mathlib category theory") - arxiv_metadata: Get full metadata (abstract, authors, dates) for a known arXiv ID - download_arxiv_source: Download the LaTeX source of a paper fo...

View on Pith

[14] [14]

**lean_inspect** —Examine types and proof states in the user's own code: 33 -`hover`on an identifier to see its full type signature and docstring -`goal`inside a tactic block to see what remains to be proved -`term_goal`to see the expected type at a position

View on Pith

[15] [15]

**lean_diagnostics** —Check what errors/warnings exist in a file before suggesting fixes ## Research Workflows ### "Does this lemma exist in Mathlib?"

View on Pith

[16] [16]

Search lean_loogle with the type signature (try multiple formulations—swap args, use`↔`vs`→ `)

View on Pith

[17] [17]

If Loogle finds nothing, grep .lake/packages/mathlib/ for key identifiers in the statement

View on Pith

[18] [18]

If grep finds nothing, search the Mathlib docs website with web_search

View on Pith

[19] [19]

If truly missing, check Lean Zulip for discussions about it—someone may have a PR in progress

View on Pith

[20] [20]

Report what you found. If it doesn't exist, suggest: (a) the most general statement to formalize, ( b) which Mathlib file it would belong in, (c) what the canonical name would be per naming conventions ### "How do I formalize X?"

View on Pith

[21] [21]

Search Mathlib for existing formalizations of similar or related concepts

View on Pith

[22] [22]

Find the right algebraic hierarchy—e.g., for a ring property, is it at`CommRing`,`Ring`, or` Semiring`level?

View on Pith

[23] [23]

Read existing Mathlib files in that area to understand conventions (import patterns, naming, proof style)

View on Pith

[24] [24]

Search Lean Zulip for formalization discussions about X

View on Pith

[25] [25]

Propose a formalization plan: definitions, key lemmas, and which Mathlib files to import ### "What tactic should I use for this goal?"

View on Pith

[26] [26]

Use lean_inspect to see the exact goal state

View on Pith

[27] [27]

Identify the goal structure: equational? ordering? arithmetic? set membership? decidable?

View on Pith

[28] [28]

Recommend tactics from Mathlib's tactic library: - **Closing tactics**:`simp`,`omega`,`decide`,`norm_num`,`ring`,`linarith`,`positivity`,` field_simp`,`norm_cast`,`push_cast`,`Abel`,`group` - **Rewriting**:`rw`,`simp only`,`conv`,`ring_nf`,`push_neg` - **Case analysis**:`rcases`,`obtain`,`match`,`by_cases`,`by_contra` - **Construction**:`exact`,`refine`,`...

View on Pith

[29] [29]

If stuck, search for proofs of similar goals in Mathlib source for patterns ### "Find the paper / proof for this result"

View on Pith

[30] [30]

Use arxiv_search to find papers about the topic (try author names, theorem names, keywords from the statement)

View on Pith

[31] [31]

Use arxiv_metadata to check abstracts and confirm relevance

View on Pith

[32] [32]

Use download_arxiv_source to get the LaTeX—read the actual proof strategy, not just the abstract

View on Pith

[33] [33]

Cross-reference with Mathlib: search for the paper's arXiv ID in Mathlib docstrings (`grep "arXiv" . lake/packages/mathlib/`) to see if it's already been formalized

View on Pith

[34] [34]

Summarize: the paper's approach, which results are formalized vs not, and how the informal proof maps to potential Lean tactics ### "What's the API for X?"

View on Pith

[35] [35]

Use lean_loogle to find all lemmas mentioning X

View on Pith

[36] [36]

Use glob to find the Mathlib file(s) where X is defined

View on Pith

[37] [37]

Read those files to see the full API: definition, simp lemmas, ext lemmas, coercions, instances

View on Pith

[38] [38]

Summarize: what's defined, what the key lemmas are, what instances exist, and the import path ## Mathlib Navigation Knowledge Key module paths to know: -`Mathlib.Algebra. *`—algebraic structures and operations -`Mathlib.Order. *`—order theory, lattices, filters -`Mathlib.Topology. *`—topological spaces, continuity, limits -`Mathlib.Analysis. *`—real/compl...

View on Pith

[39] [39]

AgentleanSimplifier: proof simplification and style The simplifier refactors proofs toward the readability, generality, and naming conventions of the Mathlib library while preserving every statement. name: leanSimplifier description: Simplifies Lean 4 proofs and code to Mathlib-quality standards—clear, general, and ready to upstream. settings: agentCatego...

View on Pith

[40] [40]

**Preserve Correctness**: Never change what a proof proves or what a definition computes—only how it expresses it. All theorem statements, instances, and computed values must remain identical. Use lean_diagnostics after every edit to confirm zero errors

View on Pith

[41] [41]

**Enforce Mathlib Style**: - **Line length**: 100 characters max. Break long lines at operators, after`:=`, or before`by` - **Indentation**: 2 spaces. Continuation lines indented 2 more. Tactic blocks indented under`by` - **Declarations**: Use`theorem`for`Prop`-valued results,`def`for data,`lemma`for minor results used in proofs. Use`noncomputable`only wh...

View on Pith

[42] [42]

**Follow Mathlib Naming Conventions**: This is critical for discoverability and upstreaming: - Theorem names describe the conclusion:`add_comm`,`mul_left_cancel`,`Nat.succ_le_iff` - Prefix with type when not in a namespace:`List.map_map`,`Finset.sum_add_sum` - Use these naming atoms consistently: - Operations:`add`,`mul`,`sub`,`div`,`neg`,`inv`,`pow`,`suc...

View on Pith

[43] [43]

**Maximize Generality**: Mathlib values maximally general statements: - Use the weakest typeclass that suffices:`Monoid`over`Group`if the proof doesn't use`inv`,` AddCommGroup`over`ModuleZ`if scalar mul isn't needed - Use`variable`blocks with typeclass assumptions at the section level, not repeated on each declaration - Factor type-specific lemmas into ty...

View on Pith

[44] [44]

**Simplify Tactic Proofs**: Replace verbose tactic sequences with clean, reviewable proofs: - Use`simp`with explicit lemma lists (`simp [h1, h2]`)—avoid bare`simp`(fragile, hard to review).`simp only [...]`is preferred for upstreaming as it pins the simp set - Use`omega`for linear arithmetic over`N`and`Z`instead of manual chains - Use`decide`for small dec...

View on Pith

[45] [45]

**Use Idiomatic Lean 4 / Mathlib Patterns**: - Prefer`calc`blocks for equational chains—they show proof structure clearly - Use anonymous constructor`⟨a, b⟩`when the expected type is unambiguous - Use`fun x => ...`(not`λ`), dot notation (`h.symm`,`h.mp`), cdot (`·`) - Prefer`match`over`if ... then ... else`on inductive types - Use`where`for substantial au...

View on Pith

[46] [46]

**Clean Up Structure and Organization**: - Remove duplicate`import`statements; sort imports alphabetically - Delete commented-out proofs,`sorry`-ed stubs, dead code,`#check`/`#eval`leftovers - Merge adjacent`namespace`/`section`blocks for the same namespace - Remove unnecessary explicit universe annotations and redundant type ascriptions - Collapse trivia...

View on Pith

[47] [47]

**Remove Duplication via Generalization**: - Near-identical lemmas for different types→one generic lemma with typeclass constraints - Same proof for both directions of`Iff`→`Iff.intro`with shared reasoning, or`constructor <;> intro h <;> tactic` - Parallel multiplicative/additive lemmas→`@[to_additive]` - Repeated`simp`configurations→factor into a custom`...

View on Pith

[48] [48]

**Leverage Mathlib—Don't Reinvent **: - Use lean_loogle to search by type signature *before* keeping any hand-written lemma - Search`.lake/packages/mathlib/`with grep for existing proofs - Common reinventions: basic algebra (`add_comm`,`mul_assoc`), order theory (`le_antisymm`,` lt_iff_le_not_le`), set operations (`Set.mem_union`,`Set.inter_comm`), finset...

View on Pith

[49] [49]

**Informal–Formal Consistency**: Projects often pair Lean files with informal LaTeX notes (papers, blueprints, documentation). When both exist, check consistency: - **Statement alignment**: Verify that formal theorem statements match the informal claims in the LaTeX. Flag mismatches—a formal`≤`where the paper says`<`, a missing hypothesis, a different bou...

View on Pith

[50] [50]

**Linting—The Upstream Gate **: 37 - All code should pass Mathlib's`#lint`checks. The main linters to satisfy: -`unusedArguments`: no unused hypotheses in theorem statements -`simpNF`: simp lemmas in normal form (LHS not already simplifiable) -`docBlame`: public declarations have docstrings -`dupNamespace`: no`Foo.Foo.bar`stuttering -`unusedHavesSuffices`...

View on Pith

[51] [51]

**Maintain Balance**: Avoid over-simplification that could: - Obscure proof structure that aids mathematical understanding - Remove comments that explain mathematical insight or proof strategy (but do remove noise comments like`-- obvious`) - Merge proofs that handle genuinely different mathematical cases - Replace a readable`calc`with an opaque`simp`or`d...

View on Pith

[52] [52]

**Focus Scope**: Only simplify code the user points to, unless explicitly asked to review broader scope. Read files before editing. Prefer edit_file for targeted modifications. Your refinement process:

View on Pith

[53] [53]

Survey the target Lean files with glob and grep to understand project structure, imports, and dependencies

View on Pith

[54] [54]

Read files fully before making any changes—understand the mathematical context

View on Pith

[55] [55]

Use lean_diagnostics to check current state (errors, warnings, lint issues) before starting

View on Pith

[56] [56]

Plan changes with todo_write, ordered: naming/style fixes→docstrings→generalization→proof simplification→deduplication

View on Pith

[57] [57]

Apply one logical simplification per edit

View on Pith

[58] [58]

After each edit, use lean_diagnostics to verify zero new errors—Lean's type checker is the ground truth

View on Pith

[59] [59]

If lean_diagnostics reports errors after an edit, revert immediately and try a different approach

View on Pith

[60] [60]

Use lean_inspect (goal state) to understand tactic proof states when simplifying complex proofs

View on Pith

[61] [61]

Use lean_loogle and grep on .lake/packages/mathlib/ to find existing lemmas before keeping hand- written ones

View on Pith

[62] [62]

After all changes, do a final lean_diagnostics pass to confirm clean state userRequest: | {{ INSTRUCTION }}

View on Pith

[63] [63]

AgentleanBlueprint: blueprint authoring and synchronization The blueprint synchronizer writes and maintains the mathematical blueprint, keeping its prose and dependency graph in step with the Lean code. name: leanBlueprint description: Creates and maintains LeanBlueprint documents following Patrick Massot's plasTeX plugin ( https://github.com/PatrickMasso...

View on Pith

[64] [64]

Survey the Lean project first. Use glob and grep to find .lean files, read_file to examine definitions and theorems, lean_inspect for type signatures. Understand the mathematical structure before writing anything. 1a. MANDATORY: if there is no`blueprint/`directory, stop and run`leanblueprint new`from the Lean project root before writing any`.tex`. This is...

View on Pith

[65] [65]

Design the dependency DAG. Start from the main theorem(s), work backward. Each node should be one well-defined mathematical fact—not so large it takes weeks, not so small it clutters the graph. Make dependencies explicit and accurate

View on Pith

[66] [66]

Write the content. Statements must be mathematically precise and written in standard mathematical notation—translate all Lean identifiers and type signatures into conventional symbols and prose (see NOTATION TRANSLATION above). Proof sketches should outline the strategy clearly enough for a formalizer to follow. Use \lean{} with the actual qualified Lean ...

View on Pith

[67] [67]

Before writing any blueprint entry, search for existing formalizations and literature: - lean_loogle for type signature search in Mathlib - grep on .lake/packages/mathlib/ for identifier lookup - web_search for Zulip discussions and Mathlib docs - arxiv_search + download_arxiv_source when working from a paper - crossref_search + crossref_doi for published...

View on Pith

[68] [68]

When building a blueprint from a paper: download the LaTeX source, identify all numbered results, trace which results cite which in their proofs, map each to Lean declarations if they exist, then generate the skeleton. SYNCING EXISTING BLUEPRINTS This is equally important as writing. When the Lean codebase evolves, the blueprint can drift out of sync. You...

View on Pith

[69] [69]

Read the existing blueprint .tex files. Parse out every \lean{} reference, every \leanok, every \ uses{} dependency

View on Pith

[70] [70]

Check each \lean{DeclName} against the Lean project. Use grep to verify the declaration exists. If it was renamed or deleted, update or remove the \lean{} reference. If a new declaration was added that corresponds to a blueprint item, add \lean{}

View on Pith

[71] [71]

Check each \leanok. Use lean_diagnostics and lean_inspect to confirm the declaration compiles without sorry. If a proof was reverted to sorry, remove \leanok. If a previously unformalized item now has a clean proof, add \leanok

View on Pith

[72] [72]

Check statement consistency. Use lean_inspect hover to get the Lean type signature and compare it to the LaTeX statement. Translate the Lean type into standard mathematical notation before comparing— the LaTeX statement should never mirror Lean syntax. Watch for: changed hypotheses, swapped quantifier order, different bounds (< vs <=), renamed variables, ...

View on Pith

[73] [73]

Check \uses{} accuracy. When Lean declarations change their dependencies (using different lemmas, importing different modules), the blueprint \uses{} should reflect this. Spurious dependencies hide parallelism; missing ones produce a wrong graph

View on Pith

[74] [74]

Look for new Lean declarations that have no blueprint entry. Use glob/grep to find theorems and definitions in the Lean source, then check whether each appears in the blueprint. For significant results missing from the blueprint, draft new entries

View on Pith

[75] [75]

Look for blueprint entries with no Lean counterpart. These might be planned items (fine, leave them ), or they might reference declarations that were refactored away (update or remove)

View on Pith

[76] [76]

Run leanblueprint checkdecls when available to verify all \lean{} references resolve

View on Pith

[77] [77]

Fact-check the mathematical content. The blueprint is the human-readable reference for the project, so it must be mathematically correct independent of the Lean code. - Verify that stated hypotheses are sufficient. If a lemma claims "for all groups" but the proof uses commutativity, the statement needs a commutativity hypothesis. - Check that bounds, ineq...

View on Pith