zampino

3 ms·

1. 1.▲
   by zampino 8y ago

   Here you have an interactive example showing how LaTTe (the lisp proof assistant written in clojure) can prove (a typed version of) Cantor Theorem on the cardinality of sets. https://news.ycombinator.com/item?id=18802480
2. 2.▲
   by zampino 8y ago

   You can sign up for a nextjournal account using the invite code curryon2018 and remix the article.
3. 3.▲
   by zampino 8y ago

   This was my very first experiment with LaTTe ( https://github.com/latte-central/LaTTe ) and with proof assistants in general. You can remix the short article in nextjournal (using the invite code curryon2018 ) to start