Every operator on the map, rated by what a
Lean proof of its formula would take.
The verified layer shows what is proven; this page shows
the rest of the terrain, one honest row per operator: proven, trivially
true, provable only with real analysis, or carrying nothing to prove.
Every number is computed at load from
the published roadmap, never
hardcoded.
The frontier, counted
The needs analysis rows are the interesting
column: Brillouin-zone sums, correlation-function integrals, and
occupation-number factors that no generator tactic closes. Each one is a
well-posed formalization project. If you work on formal mathematics for
physics and one of these rows is your kind of problem, the
repository
is open, and the generated Lean sources compile against
physlib
with two commands.