Comment by bayesnet

I’ve written a lot of Lean for economic modeling (so take this with the caveat that it’s not frontier-level mathematics research) but I think this problem is overstated. If you follow good engineering standards—keep primitives composable and design abstraction well—it’s not so hard to understand enough Lean to ensure the formalized statement is correct.

In part this is possible because mathlib is very well-designed and has a very good API (in no small part because they’re willing to make breaking changes all the time), so building on top of it makes life much easier.