3 ms·
It is funny that Z3 was done by the Lean guy. But it probably also explains that Lean basically switched to classical logic.
by auggierose 2y ago
It is funny that Z3 was done by the Lean guy. But it probably also explains that Lean basically switched to classical logic.
- hackandthink 2y agoThere 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...
- auggierose 2y agoYes, I know him.