Are you familiar with homotopy type theory? One of its proponents, Fields medalist Vladimir Voevodsky, has stated that his contributions are part of a “personal mission” to bring mathematics into a new age of formal verification [1]. I’d be curious to know how this compares to LEAN.
[1] https://www.ias.edu/ideas/2014/voevodsky-origins