{"id":1455,"date":"2014-03-19T22:30:18","date_gmt":"2014-03-19T21:30:18","guid":{"rendered":"http:\/\/cerezo.name\/blog\/?p=1455"},"modified":"2024-10-14T13:28:03","modified_gmt":"2024-10-14T11:28:03","slug":"assorted-links-maths-2","status":"publish","type":"post","link":"https:\/\/cerezo.name\/blog\/2014\/03\/19\/assorted-links-maths-2\/","title":{"rendered":"Assorted Links (Maths)"},"content":{"rendered":"<ul>\n<li style=\"text-align: justify;\">The 2013 Turing Award goes to <a href=\"http:\/\/www.lamport.org\/\" target=\"_blank\" rel=\"noopener\" class=\"broken_link\">Leslie Lamport<\/a>, author of LaTeX and the <a href=\"http:\/\/en.wikipedia.org\/wiki\/Paxos_(computer_science)\" target=\"_blank\" rel=\"noopener\">Paxos family of protocols<\/a><\/li>\n<li style=\"text-align: justify;\">The research program <em><a href=\"http:\/\/www.math.ias.edu\/~vladimir\/Site3\/Univalent_Foundations.html\" target=\"_blank\" rel=\"noopener\">Univalent Foundations of Mathematics<\/a><\/em> by the famed Vladimir Voevodsky is a really ambitious one: it would revolutionise automated theorem proving<\/li>\n<li style=\"text-align: justify;\">A <a href=\"http:\/\/www.nicta.com.au\/pub?doc=6061\" target=\"_blank\" rel=\"noopener\">mechanised proof of Fermat\u2019s Little Theorem<\/a> (<span class=\"caps\">HOL4<\/span>)<\/li>\n<li style=\"text-align: justify;\">I have recently learnt that the beautiful books [amazon_link id=\u201c0883857006\u201d target=\u201c_blank\u201d ]Proofs without Words I[\/amazon_link]&nbsp;and&nbsp;[amazon_link id=\u201c0883857219\u201d target=\u201c_blank\u201d ]Proofs without Words <span class=\"caps\">II<\/span>[\/amazon_link] by Roger B. Nelsen have an historical precedent from a more impressive mid-19<sup class=\"ordinal\">th<\/sup> century book:&nbsp;<a href=\"http:\/\/www.math.ubc.ca\/~cass\/Euclid\/byrne.html\" target=\"_blank\" rel=\"noopener\">Oliver Byrne\u2019s edition of Euclid<\/a>.<\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>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\u2019s Little Theorem (<span class=\"caps\">HOL4<\/span>) I have recently learnt that the beautiful&nbsp;[\u2026]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"wp_typography_post_enhancements_disabled":false,"ngg_post_thumbnail":0},"categories":[18,9],"tags":[],"_links":{"self":[{"href":"https:\/\/cerezo.name\/blog\/wp-json\/wp\/v2\/posts\/1455"}],"collection":[{"href":"https:\/\/cerezo.name\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/cerezo.name\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/cerezo.name\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/cerezo.name\/blog\/wp-json\/wp\/v2\/comments?post=1455"}],"version-history":[{"count":3,"href":"https:\/\/cerezo.name\/blog\/wp-json\/wp\/v2\/posts\/1455\/revisions"}],"predecessor-version":[{"id":1536,"href":"https:\/\/cerezo.name\/blog\/wp-json\/wp\/v2\/posts\/1455\/revisions\/1536"}],"wp:attachment":[{"href":"https:\/\/cerezo.name\/blog\/wp-json\/wp\/v2\/media?parent=1455"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/cerezo.name\/blog\/wp-json\/wp\/v2\/categories?post=1455"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/cerezo.name\/blog\/wp-json\/wp\/v2\/tags?post=1455"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}