@antidote @isAdisplayName @rahulc29 Since I've said some negative things, let me say some positive things about Lean.
The tooling is simply amazing, and it is getting better and better. The libraries (like mathlib) are really impressive. A huge cultural improvement introduced by Lean over Coq is to prioritise a system where you can do classical mathematics without friction. (It's of course possible in Coq, but you have to step through all these bizarre French Constructivist nomenclatures and mistaken or archaic ideas about constructivity, etc...)
=> More informations about this toot | View the thread | More toots from jonmsterling@mathstodon.xyz
=> View antidote@mathstodon.xyz profile | View isAdisplayName@mathstodon.xyz profile | View rahulc29@mathstodon.xyz profile
text/geminiThis content has been proxied by September (3851b).