You're touching on something that's boosted the progress of languages with proof capabilities such as Spark and Frama-C. They standardized around the use of why

You're touching on something that's boosted the progress of languages with proof capabilities such as Spark and Frama-C. They standardized around the use of why3, and use it as a lever to harness state of the art SMT engines (z3, cvc4, alt-ergo) but also advanced specific provers on specific theories (floating point in particular, I'm thinking of gappa, the amazing work of the toccata lab, and Altran UK making incredible strides in the last 5 years). As soon as a new proving tool is plugged in why, you can harness it. And they built bridges for interactive proof with coq and Isabelle, but also with static analysis tools like codepeer. Why3 is a big success in the way you're asking. Just not adapted to pure maths proof like lean.