Post #2121599
2026-04-24 15:05 UTC
https://lawrencecpaulson.github.io/2026/04/23/Why_not_Lean.html
Replies (3)
-
@MartinEscardo@mathstodon.xyz 2026-04-24 17:36
@ltchen@mathstodon.xyz There are so many things to agree and disagree in Paulson's post.
-
@soaproot@sfba.social 2026-04-25 00:28
@ltchen@mathstodon.xyz I'm apparently the sort of person who would pick up a book and immediately look for my name in the index, at least in the sense that my first reaction as I was reading this post was to see whether Metamath was in the list of systems discussed. (It is not.)
-
@chrisamaphone@hci.social 2026-04-26 04:22
@ltchen@mathstodon.xyz do you know what he's saying about "putting proof kernels inside abstract data types" in ML?