Comment by trevyn

>So even when it compiles, you’ve got the burden of verifying everything is above board which is a pretty huge task.

Is this true?

e.g. the Riemann hypothesis is in mathlib:

  def RiemannHypothesis : Prop :=
    ∀ (s : ℂ) (_ : riemannZeta s = 0) (_ : ¬∃ n : ℕ, s = -2 * (n + 1)) (_ : s ≠ 1), s.re = 1 / 2

If I construct a term of this type without going via one of the (fairly obvious) soundness holes or a compiler bug, it's very likely proved, no? No matter how inscrutable the proof is from a mathematical perspective. (Translating it into something mathematicians understand is a separate question, but that's not really what I'm asking.)