LeanArchitect: Automating Blueprint Generation for Humans and AI

TL;DR

LeanArchitect is a new tool that automates the creation and management of blueprints in Lean formalization projects, reducing manual effort and improving integration with AI theorem proving.

Contribution

It introduces a declarative annotation system and automated dependency inference for blueprints directly within Lean, streamlining formal-informal documentation and AI collaboration.

Findings

Automated conversion of large blueprint-driven projects

Improved maintainability and consistency detection

Enhanced integration of AI tools in formalization workflows

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.