For those who like proof assistants, this is cool: https://nextjournal.com/zampino/latte-cantor
Proving Cantor's Theorem in Clojure Using LaTTe *LaTTe* <https://github.com/latte-central/LaTTe>* is a Lisp proof assistant based on the typed lambda calculus **System-F* <https://en.wikipedia.org/wiki/System_F>*. It is written in Clojure and exposes a powerful DSL for expressing the basic terms of mathematical reasoning: definitions, axioms, theorems, and proofs. In this short article we're showing how LaTTe can prove — ad absurdum of course — the well known Cantor inequality using the diagonal method. In words, given a type T, there have to be strictly more sets (predicates) over T than inhabitants of T itself. This not hard to prove on paper, indeed **just three lines* <https://en.wikipedia.org/wiki/Cantor%27s_theorem#Proof>*, but it's awesome to see how LaTTe verifies the natural logical steps to obtain the very same proof.* - pt -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to everything-list+unsubscr...@googlegroups.com. To post to this group, send email to everything-list@googlegroups.com. Visit this group at https://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/d/optout.
