LeanArchitect: Automating Blueprint Generation for Humans and AI

TL;DR

LeanArchitect introduces a Lean-native blueprint framework that binds informal LaTeX blueprints to formal Lean declarations via a new @[blueprint] attribute and an environment extension. By automatically inferring dependencies and proof status and exporting synchronized LaTeX fragments, it unifies formal and informal views and enables AI-assisted formalization within real projects. Case studies show seamless migration of large blueprint-driven developments, improved maintainability, and a practical two-system pipeline for autoformalization of a nontrivial multivariate Taylor theorem. The approach highlights practical gains in collaboration between humans and AI while identifying realistic limitations in tooling and workflow integration. Overall, LeanArchitect provides a scalable interface to manage large formalization efforts and to harness AI capabilities without duplicating effort across LaTeX and Lean codebases.

Abstract

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.

Figures (3)

• Figure 1: Comparison of blueprint generation workflows with and without using LeanArchitect. (a) Without LeanArchitect, the entire LaTeX blueprint needs to be manually written and synchronized with the evolving formalization part. (b) With LeanArchitect, maintainers only need to manually write the structure of the LaTeX blueprint, whose dependency relations and formalization status are automatically synchronized from the corresponding Lean part.
• Figure 2: Progress of blueprint-based autoformalization for multivariate Taylor's theorem. Blue nodes are unproved lemmas; green nodes are proved lemmas. Rectangles denote definitions; circles denote theorems.
• Figure 3: The blueprint generated from the example Lean file (\ref{['lean-example']}).