>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

>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.)