Counts by difficulty
The rows marked "Needs analysis" hold Brillouin-zone sums, correlation-function integrals and occupation-number factors. Each is a well-posed formalization project. A row is marked proven when a compiled bridge in lean/bridge proves a statement about its formula, under the conditions the bridge page lists. If one of the open rows is a problem you work on, the repository is open, and lean/bridge builds against Physlib with lake exe cache get and lake build.