Empirical Proof Complexity of a Lean 4 Formalization of Birch-Swinnerton-Dyer
Mathematics verified. Core theorems are machine-checked in Lean 4.
Prose and presentation may not have been human-reviewed.
Summary
We record empirical complexity measurements for the current Lean 4 formalization of the Birch-Swinnerton-Dyer conjecture and its surrounding theory.
Length
1,688 words
Status
Sketch
Target
(internal research sketch)