For those who like proof assistants, this is cool:

Proving Cantor's Theorem in Clojure Using LaTTe

*LaTTe* <>* is a Lisp proof assistant 
based on the typed lambda calculus **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* 
<>*, but it's awesome 
to see how LaTTe verifies the natural logical steps to obtain the very same 

- 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 post to this group, send email to
Visit this group at
For more options, visit

Reply via email to