There ist Jeremy Avigad's influence. He is not the typical type theorist and definitely no constructive zealot. "I have been contributing to the development of

There ist Jeremy Avigad's influence. He is not the typical type theorist and definitely no constructive zealot. "I have been contributing to the development of the Lean Theorem Prover since its inception. I led the development of the first libraries and documentation.." "Many parts of classical mathematics, however, have not been developed constructively." https://www.andrew.cmu.edu/user/avigad/research.html https://www.andrew.cmu.edu/user/avigad/research.html https://www.andrew.cmu.edu/user/avigad/Teaching/classical.pdf https://www.andrew.cmu.edu/user/avigad/Teaching/classical.pd...