← All papers
First page of LeanArchitect: Automating Blueprint Generation for Humans and AI

LeanArchitect: Automating Blueprint Generation for Humans and AI

Thomas Zhu, Pietro Monticone, Jeremy Avigad, Sean Welleck

cs.LO Jan 30, 2026 · v1
A Lean package that extracts and manages blueprint dependency graphs directly from annotated Lean declarations, generating synchronized LaTeX blueprints.
Large-scale formalization projects in Lean rely on blueprints: structured dependency graphs linking informal mathematical exposition to formal declarations. While blueprints are central to human collaboration, existing tooling treats the informal ($\LaTeX$) and formal (Lean) components as largely decoupled artifacts, leading to maintenance overhead and limiting integration with AI automation. We present LeanArchitect, a Lean package for extracting, managing, and exporting blueprint data directly from Lean code. LeanArchitect introduces a declarative annotation mechanism that associates formal declarations with blueprint metadata, automatically infers dependency information, and generates $\LaTeX$ blueprint content synchronized with the Lean development. This design eliminates duplication between formal and informal representations and eases fine-grained progress tracking for both human contributors and AI-based theorem provers. We demonstrate the practicality of LeanArchitect through the automated conversion of several large existing blueprint-driven projects, and through a human--AI collaboration case study formalizing a multivariate Taylor theorem. Our results show that LeanArchitect improves maintainability, exposes latent inconsistencies in existing blueprints, and provides an effective interface for integrating AI tools into real-world formalization workflows.

Large-scale Lean formalization projects rely on blueprints (structured dependency graphs linking informal mathematics to formal declarations), but existing tooling treats LaTeX and Lean components as decoupled artifacts, causing maintenance overhead and limiting AI integration.

The authors present LeanArchitect, a Lean package that extracts, manages, and exports blueprint data directly from Lean code. It introduces a declarative annotation mechanism associating formal declarations with blueprint metadata (informal descriptions, dependency relations, completion status) inside the Lean source. This eliminates the need to maintain separate LaTeX blueprint files and enables automated dependency tracking. The system was adopted by the PrimeNumberTheoremAnd project.

LeanArchitect was adopted as primary blueprint infrastructure by the PrimeNumberTheoremAnd project (migrated January 2026), replacing a custom extraction tool. It eliminates manual maintenance of metadata such as leanok and uses annotations while supporting many-to-one correspondence from Lean declarations to blueprint nodes.