> Especially with computer proof systems growing in popularity there's an increase in the interest in constructive methods. I think one big reason Lean is much

> Especially with computer proof systems growing in popularity there's an increase in the interest in constructive methods. I think one big reason Lean is much more popular among mathematicians than Coq ever was is that Lean is pretty unabashedly classical (that, and mathlib). That said, for people who care about program verification, Coq might be the better choice. I'm not anti-constructivism where it makes sense.