{"id":598,"date":"2020-02-24T14:30:28","date_gmt":"2020-02-24T13:30:28","guid":{"rendered":"http:\/\/owlofminerva.net\/kubota\/?page_id=598"},"modified":"2023-01-05T19:05:02","modified_gmt":"2023-01-05T18:05:02","slug":"update-to-the-foundations-of-mathematics","status":"publish","type":"page","link":"https:\/\/owlofminerva.net\/kubota\/update-to-the-foundations-of-mathematics\/","title":{"rendered":"Update to the &#8220;Foundations of Mathematics&#8221;"},"content":{"rendered":"\n<p>Some updates to the <a href=\"https:\/\/doi.org\/10.4444\/100.111\">\u201cFoundations of Mathematics\u201d<\/a>:<\/p>\n\n\n\n<ul class=\"wp-block-list\">\n<li>General debate initiated by Kevin Buzzard on formalizing mathematics: <a rel=\"noreferrer noopener\" aria-label=\"Where is the fashionable mathematics? (opens in a new tab)\" href=\"https:\/\/xenaproject.wordpress.com\/2020\/02\/09\/where-is-the-fashionable-mathematics\/\" target=\"_blank\">Where is the fashionable mathematics?<\/a> (Feb. 2020)\n<ul class=\"wp-block-list\">\n<li><a rel=\"noreferrer noopener\" aria-label=\"Reply to Kevin Buzzard (opens in a new tab)\" href=\"https:\/\/groups.google.com\/d\/msg\/metamath\/Fgn0qZEzCko\/bvVem1BZCQAJ\" target=\"_blank\">My comment on Kevin Buzzard&#8217;s intervention<\/a> (Feb. 2020)<\/li>\n\n\n\n<li>Discussion links: <a href=\"https:\/\/twitter.com\/XenaProject\/status\/1226561593581932546\" target=\"_blank\" rel=\"noreferrer noopener\" aria-label=\"Twitter (opens in a new tab)\">Twitter<\/a>, <a rel=\"noreferrer noopener\" aria-label=\"Y Combinator (opens in a new tab)\" href=\"https:\/\/news.ycombinator.com\/item?id=22390486\" target=\"_blank\">Y Combinator<\/a>, <a href=\"https:\/\/groups.google.com\/d\/msg\/lean-user\/IiDrggIXwdU\/augWMR7FGgAJ\" target=\"_blank\" rel=\"noreferrer noopener\" aria-label=\"Lean (opens in a new tab)\">Lean<\/a>, <a rel=\"noreferrer noopener\" aria-label=\"Metamath (opens in a new tab)\" href=\"https:\/\/groups.google.com\/d\/msg\/metamath\/uVkxMJGwReU\/qxQrQBQ3BQAJ\" target=\"_blank\">Metamath<\/a><\/li>\n<\/ul>\n<\/li>\n\n\n\n<li><a rel=\"noreferrer noopener\" aria-label=\"Lean (opens in a new tab)\" href=\"https:\/\/leanprover.github.io\" target=\"_blank\">Lean<\/a> theorem prover (Feb. 2020)<\/li>\n\n\n\n<li><a href=\"http:\/\/www.fstar-lang.org\" target=\"_blank\" rel=\"noreferrer noopener\">F*<\/a> (Jan. 2023)<\/li>\n<\/ul>\n\n\n\n<p><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Some updates to the \u201cFoundations of Mathematics\u201d:<\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":111,"comment_status":"closed","ping_status":"closed","template":"","meta":{"sfsi_plus_gutenberg_text_before_share":"","sfsi_plus_gutenberg_show_text_before_share":"","sfsi_plus_gutenberg_icon_type":"","sfsi_plus_gutenberg_icon_alignemt":"","sfsi_plus_gutenburg_max_per_row":"","footnotes":""},"class_list":["post-598","page","type-page","status-publish","hentry","post-preview"],"_links":{"self":[{"href":"https:\/\/owlofminerva.net\/kubota\/wp-json\/wp\/v2\/pages\/598","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/owlofminerva.net\/kubota\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/owlofminerva.net\/kubota\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/owlofminerva.net\/kubota\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/owlofminerva.net\/kubota\/wp-json\/wp\/v2\/comments?post=598"}],"version-history":[{"count":18,"href":"https:\/\/owlofminerva.net\/kubota\/wp-json\/wp\/v2\/pages\/598\/revisions"}],"predecessor-version":[{"id":747,"href":"https:\/\/owlofminerva.net\/kubota\/wp-json\/wp\/v2\/pages\/598\/revisions\/747"}],"wp:attachment":[{"href":"https:\/\/owlofminerva.net\/kubota\/wp-json\/wp\/v2\/media?parent=598"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}