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.

翻译：在Lean中进行大规模形式化项目依赖于蓝图：这是一种将非形式化的数学阐述与形式化声明相连接的结构化依赖图。虽然蓝图对于人类协作至关重要，但现有工具将非形式化（$\LaTeX$）与形式化（Lean）组件视为基本解耦的产物，导致维护开销增加并限制了与AI自动化工具的集成。本文提出LeanArchitect——一个直接从Lean代码中提取、管理和导出蓝图数据的Lean软件包。LeanArchitect引入了一种声明式标注机制，将形式化声明与蓝图元数据相关联，自动推断依赖信息，并生成与Lean开发同步的$\LaTeX$蓝图内容。该设计消除了形式化与非形式化表示之间的重复，并为人类贡献者和基于AI的定理证明器提供了细粒度的进度跟踪支持。我们通过自动化转换多个现有的大型蓝图驱动项目，以及通过一个形式化多元泰勒定理的人机协作案例研究，证明了LeanArchitect的实用性。实验结果表明，LeanArchitect提升了可维护性，揭示了现有蓝图中潜在的逻辑不一致性，并为将AI工具集成到实际形式化工作流程提供了有效接口。