LeanArchitect: Automating Blueprint Generation for Humans and AI
Thomas Zhu, Pietro Monticone, Jeremy Avigad, Sean Welleck

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 () 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 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…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsScientific Computing and Data Management · Logic, programming, and type systems · Mathematics, Computing, and Information Processing
