- 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 [amazon_link id=“0883857006” target=“_blank” ]Proofs without Words I[/amazon_link] and [amazon_link id=“0883857219” target=“_blank” ]Proofs without Words II[/amazon_link] by Roger B. Nelsen have an historical precedent from a more impressive mid-19th century book: Oliver Byrne’s edition of Euclid.
Assorted Links (Maths)
Leave a reply