{"id":9276,"date":"2020-11-12T13:28:46","date_gmt":"2020-11-12T18:28:46","guid":{"rendered":"https:\/\/irreal.org\/blog\/?p=9276"},"modified":"2020-11-12T13:31:28","modified_gmt":"2020-11-12T18:31:28","slug":"lean-and-the-mathematical-library-of-the-future","status":"publish","type":"post","link":"https:\/\/irreal.org\/blog\/?p=9276","title":{"rendered":"Lean and the Mathematical Library of the Future"},"content":{"rendered":"<p>Over at <a href=\"https:\/\/www.quantamagazine.org\">Quanta<\/a> magazine, Kevin Hartnett has an <a href=\"https:\/\/www.quantamagazine.org\/building-the-mathematical-library-of-the-future-20201001\/\">interesting article<\/a> about using computers in the service of Mathematics. That\u2019s nothing new, of course, but this isn\u2019t about numerical methods or LaTeX, it\u2019s about using computers to help develop mathematical proofs.<\/p>\n<p>Even that notion isn\u2019t new. There is, for instance, <a href=\"https:\/\/en.wikipedia.org\/wiki\/Coq\">Coq<\/a>, which has been doing the same sort of thing since 1989. What is new is that Mathematicians are trying to capture within another theorem prover, <a href=\"https:\/\/en.wikipedia.org\/wiki\/Lean_(proof_assistant)\">Lean<\/a>, all known mathematics, or at least all of undergraduate mathematics. That\u2019s a huge undertaking and they\u2019re still only about half done. The hope is that with that knowledge, Lean will know enough to start help proving theorems.<\/p>\n<p>According to the latest <a href=\"https:\/\/leanprover-community.github.io\/mathlib_stats.html\">Mathlib Statistics<\/a>, there are currently 19,305 definitions and 41,552 theorems in the system. You can, yourself, play with the system if you like. There are instructions for <a href=\"https:\/\/leanprover-community.github.io\/get_started.html\">installing it<\/a> on all of the usual operating systems or even for <a href=\"https:\/\/leanprover-community.github.io\/lean-web-editor\/#url=https%3A%2F%2Fraw.githubusercontent.com%2Fleanprover-community%2Ftutorials%2Fmaster%2Fsrc%2Fexercises%2F00_first_proofs.lean\">running it in a browser<\/a>, although that will be much slower than a regular installation.<\/p>\n<p>If, like many of us, you come from a Mathematical background, you\u2019ll probably find the article interesting and may want to try the system out.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Over at Quanta magazine, Kevin Hartnett has an interesting article about using computers in the service of Mathematics. That\u2019s nothing new, of course, but this isn\u2019t about numerical methods or LaTeX, it\u2019s about using computers to help develop mathematical proofs. &hellip; <a href=\"https:\/\/irreal.org\/blog\/?p=9276\">Continue reading <span class=\"meta-nav\">&rarr;<\/span><\/a><\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","ping_status":"closed","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[5],"tags":[37],"class_list":["post-9276","post","type-post","status-publish","format-standard","hentry","category-general","tag-tech"],"_links":{"self":[{"href":"https:\/\/irreal.org\/blog\/index.php?rest_route=\/wp\/v2\/posts\/9276","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/irreal.org\/blog\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/irreal.org\/blog\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/irreal.org\/blog\/index.php?rest_route=\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/irreal.org\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=9276"}],"version-history":[{"count":2,"href":"https:\/\/irreal.org\/blog\/index.php?rest_route=\/wp\/v2\/posts\/9276\/revisions"}],"predecessor-version":[{"id":9278,"href":"https:\/\/irreal.org\/blog\/index.php?rest_route=\/wp\/v2\/posts\/9276\/revisions\/9278"}],"wp:attachment":[{"href":"https:\/\/irreal.org\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=9276"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/irreal.org\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=9276"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/irreal.org\/blog\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=9276"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}