Post #2693633
2026-04-25 15:17 UTC
@fl@mathstodon.xyz @Jose_A_Alonso@mathstodon.xyz
I have long been an admirer of Paulson’s work, decades long, in fact. He wrote my favourite programming book on my favourite programming language. So my views maybe biased in Paulson’s favour.
Having said that, I agree with his position, specifically about the cultism surrounding Lean—it’s mathematicians’ Python. On the other hand, cultism does not automatically negate the intrinsic value of Python and Lean.
No matter the momentum, we each make exercise our independent judgment. That is why I’m with Paulson.
PS: I am a staunch Agda fan.
Replies (1)
-
@fl@mathstodon.xyz 2026-04-25 18:12
@AmenZwa@mathstodon.xyz @Jose_A_Alonso@mathstodon.xyz I've never understood why Lean is so in favor with mathematicians. Is there something in this proof checker that doesn't exist in the others ? Or do mathematicians follow the fashion? Isabelle has suffered from the poor quality of its documentation, especially its tutorial, in my opinion.