Assorted Links (Maths) | David Cerezo Sánchez

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-19^th century book: Oliver Byrne’s edition of Euclid.