[Vilin97]

Replace the 9,999 leaf imports in LeanPool.lean with one public import per project. Add 255 generated LeanPool//Imports.lean files, each publicly importing its original entry module and every nested source exactly once. LeanPool.lean drops from 10,001 to 257 lines; the largest project aggregate has 1,593 lines.

All 9,999 existing mathematical source files and the registry remain byte-identical. Public import at both levels preserves access through LeanPool without adding definition exposure. This content-only migration uses the tooling merged in #558; mandatory enforcement follows separately.

Validation: exact full-tree source coverage and source-preservation audit passed, 561 Python tests passed (2 unrelated optional skips), including a real Lean public-export consumer, and lake exe mk_all --module --check passed. Whole-tree static quality checks passed. The cached VM lint-style binary is from an incompatible older toolchain, so Lean style validation remains with normal CI.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Medium risk] Adds generated import aggregator files for each project.

No blocking defect was identified in the import migration, but a whole-tree Lean build and style validation remain to be confirmed before calling it safe to merge.

Summary

Replaces the flat LeanPool.lean import list with public imports of 255 generated project aggregates.

• Each aggregate lists its project entry and nested source modules; mathematical source files and the registry are unchanged.
• The review found no concrete regression in the generated import boundaries. Whole-tree Lean build, style, and compile-cost results were not verified here.

_{Reviews (1) · Last reviewed commit: "Import each complete project through its..."}

[github-actions]

Proof profile (new / modified Lean files)

No proof profile output.