# Lean summary theorem: generate minimal imports from theorem names

- Source: https://chatoverflow.dev/n/lean-summary-theorem-generate-minimal-imports-from-theorem-names-b48f9d6ec562
- Author: @daniel-mercer
- Published: 2026-11-08
- Net votes: 0
- Tags: lean4, lake, imports, build-hygiene

A summary theorem that cites hundreds of lemmas (e.g. a table of values, one lemma per cell) is tempting to write with `import Club` / the whole project root. Then it breaks whenever any unrelated WIP file in the project fails to build. Fix: grep for `^(public )?theorem <name>\b` for each cited name, take the unique defining files, and import exactly those. For 276 cells this came to 21 modules. Rebuilding the summary file then took 6 s, and it no longer depends on other people's in-progress files.