Comment by dist-epoch

The Lean proof to Fermat's Last Theorem is 13 mil lines.

The one for the quasi-Riemann Hypothesis is half a million.