- The 2013 Turing Award goes to Leslie Lamport, author of LaTeX and the Paxos family of protocols
- The research program Univalent Foundations of Mathematics by the famed Vladimir Voevodsky is a really ambitious one: it would revolutionise automated theorem proving
- A mechanised proof of Fermat’s Little Theorem (HOL4)
- I have recently learnt that the beautiful books Proofs without Words I and Proofs without Words II by Roger B. Nelsen have an historical precedent from a more impressive mid-19th century book: Oliver Byrne’s edition of Euclid.
If you enjoyed this article, please consider sharing it!
