{"id":3271,"date":"2024-05-11T23:11:35","date_gmt":"2024-05-11T15:11:35","guid":{"rendered":"https:\/\/www.shuizilong.com\/house\/?p=3271"},"modified":"2024-05-13T15:51:46","modified_gmt":"2024-05-13T07:51:46","slug":"lean-the-proof-assistant","status":"publish","type":"post","link":"https:\/\/www.shuizilong.com\/house\/archives\/lean-the-proof-assistant\/","title":{"rendered":"Lean \u76f8\u5173"},"content":{"rendered":"<p>\u7531\u4e8e\u5404\u81ea\u4e0d\u540c\u7684\u539f\u56e0\uff0c\u53d1\u73b0\u5927\u5bb6\u8fd9\u4e2a\u5b66\u671f\u90fd\u5f00\u59cb\u5b66\u4e60\u8d77 Lean \u4e86\u8d77\u6765\uff0c\u6211\u4e5f\u4e0d\u80fd\u514d\u4fd7\u56e7\u3002L\u2203\u2200N \u4e00\u770b logo \u5c31\u5f88\u5e05\uff0c\u6709\u70b9 DUNE \u7684\u8bbe\u8ba1\u611f\u6709\u6ca1\u6709\uff1f<\/p>\n<p><a href=\"https:\/\/www.shuizilong.com\/house\/wp-content\/uploads\/2024\/05\/2024-05-12-02.41.40.jpg\"><img loading=\"lazy\" decoding=\"async\" data-attachment-id=\"3287\" data-permalink=\"https:\/\/www.shuizilong.com\/house\/archives\/lean-the-proof-assistant\/2024-05-12-02-41-40\/\" data-orig-file=\"https:\/\/www.shuizilong.com\/house\/wp-content\/uploads\/2024\/05\/2024-05-12-02.41.40.jpg\" data-orig-size=\"462,124\" data-comments-opened=\"1\" data-image-meta=\"{&quot;aperture&quot;:&quot;0&quot;,&quot;credit&quot;:&quot;&quot;,&quot;camera&quot;:&quot;&quot;,&quot;caption&quot;:&quot;&quot;,&quot;created_timestamp&quot;:&quot;0&quot;,&quot;copyright&quot;:&quot;&quot;,&quot;focal_length&quot;:&quot;0&quot;,&quot;iso&quot;:&quot;0&quot;,&quot;shutter_speed&quot;:&quot;0&quot;,&quot;title&quot;:&quot;&quot;,&quot;orientation&quot;:&quot;0&quot;}\" data-image-title=\"2024-05-12 02.41.40\" data-image-description=\"\" data-image-caption=\"\" data-medium-file=\"https:\/\/www.shuizilong.com\/house\/wp-content\/uploads\/2024\/05\/2024-05-12-02.41.40.jpg\" data-large-file=\"https:\/\/www.shuizilong.com\/house\/wp-content\/uploads\/2024\/05\/2024-05-12-02.41.40.jpg\" src=\"https:\/\/www.shuizilong.com\/house\/wp-content\/uploads\/2024\/05\/2024-05-12-02.41.40.jpg\" alt=\"\" width=\"462\" height=\"124\" class=\"aligncenter size-full wp-image-3287\" \/><\/a><\/p>\n<p>\u611f\u89c9\u9996\u8981\u5de5\u4f5c\u662f\u5148\u590d\u4e60\u4e00\u4e0b <a href=\"https:\/\/www.shuizilong.com\/house\/archives\/haskell-stuff\/\">Haskell<\/a>\uff0c\u8fd9\u6837\u4e5f\u4e0d\u5fc5\u4e2d\u9014\u7ffb\u9605\u8bed\u6cd5\u624b\u518c\u3002\u663e\u7136 Lean4 \u4ece Haskell \u91cc\u501f\u9274\u4e86\u76f8\u5f53\u591a\u7684\u8bed\u6cd5\u548c\u8bbe\u8ba1\u601d\u60f3\uff0c\u8bf4\u6765\u60ed\u6127\uff0c\u867d\u7136\u6211\u4e4b\u524d\u8bd5\u56fe\u7528 Haskell \u5237\u5237\u9898\uff0c\u4f46\u662f\u603b\u662f\u611f\u89c9\u4e0d\u5f97\u8981\u9886\uff0c\u88ab\u590d\u6742\u5ea6\u5361\u7684\u6b7b\u6b7b\u7684\u56e7\u4e0d\u5f97\u4e0d\u4e2d\u9014\u5207\u56de cpp \u8279\u3002<a href=\"https:\/\/hackage.haskell.org\/package\/fingertree-0.1.5.0\/docs\/Data-FingerTree.html\">fingertree \u4ec0\u4e48\u7684<\/a>\u4e5f\u770b\u7684\u4e91\u91cc\u96fe\u91cc\uff0c\u611f\u89c9\u8fd8\u662f\u6211\u7684\u59ff\u52bf\u6c34\u5e73\u4e0d\u591f\uff0c\u8fd8\u9700\u7279\u522b\u52aa\u529b\uff01<\/p>\n<p>\u7136\u540e\u521d\u5b66 Lean \u6211\u662f\u5efa\u8bae\u5148\u770b <a href=\"https:\/\/leanprover-community.github.io\/mathematics_in_lean\/\">Mathematics in Lean<\/a>\uff0c\u672c\u4e66\u76f4\u63a5\u4f7f\u7528 mathlib\uff0c\u8ba9\u4f60\u4e0d\u5fc5\u8fc7\u65e9\u7684\u88ab\u7ec6\u8282\u529d\u9000\uff0c\u53c8\u53ef\u4ee5\u987a\u4fbf\u590d\u4e60\u4e00\u4e0b\u719f\u6089\u7684\u6570\u5b66\u77e5\u8bc6\uff08\u521d\u7b49\u6570\u8bba\u5979\u4e0d\u9999\u5417\uff0c\u5929\u5929\u5b66\u4ee3\u6570\u4eba\u90fd\u5b66\u50bb\u4e86\uff09\u3002\u800c\u4e14\u8fd8\u63d0\u4f9b\u5bf9\u5e94\u7684 <a href=\"https:\/\/github.com\/leanprover-community\/mathematics_in_lean\">Github \u4ed3\u5e93<\/a>\uff0c\u53ef\u4ee5 step-by-step \u8fb9\u770b\u522b\u6539\u3002Lean \u4e0d\u80fd\u6ca1\u6709 mathlib\uff0c\u5c31\u50cf\u662f cpp \u4e0d\u80fd\u6ca1\u6709 std\uff0c\u897f\u65b9\u4e0d\u80fd\u6ca1\u6709\u8036\u8def\u6492\u51b7\uff1f<\/p>\n<p>\uff08\u76ee\u524d\u611f\u89c9\u8fd9\u8bed\u8a00\u9664\u4e86\u4f18\u5316\u4e0d\u884c\u54ea\u54ea\u90fd\u8fd8\u53ef\u4ee5\uff1f\uff09<\/p>\n<p>\u518d\u7136\u540e\u611f\u89c9\u53ef\u4ee5\u8bd5\u8bd5\u5199\u70b9\u9898\u76ee\uff0c\u6bd4\u5982\u53ef\u4ee5\u8bd5\u8bd5\u5148\u8bc1\u660e\u9759\u6001\u76f4\u5f84\u7b97\u6cd5\uff1f<\/p>\n<h2>\u5b66\u4e60<\/h2>\n<ul>\n<li><a href=\"https:\/\/en.wikipedia.org\/wiki\/Lean_(proof_assistant)\">Lean (proof assistant), Wikipedia<\/a><\/li>\n<li><a href=\"https:\/\/leanprover-community.github.io\/learn.html\">https:\/\/leanprover-community.github.io\/learn.html<\/a><\/li>\n<li><a href=\"https:\/\/lean-fro.org\/\">Lean Focused Research Organization<\/a><\/li>\n<li><a href=\"https:\/\/leanprover.github.io\/theorem_proving_in_lean\/index.html\">Theorem Proving in Lean<\/a><\/li>\n<li><a href=\"https:\/\/leanprover-community.github.io\/mathematics_in_lean\/\">Mathematics in Lean<\/a><\/li>\n<li><a href=\"https:\/\/ammkrn.github.io\/type_checking_in_lean4\/\">Type Checking in Lean 4<\/a><\/li>\n<li><a href=\"https:\/\/lean-lang.org\/functional_programming_in_lean\/\">Functional Programming in Lean<\/a><\/li>\n<li><a href=\"https:\/\/lean-lang.org\/lean4\/doc\/\">https:\/\/lean-lang.org\/lean4\/doc\/<\/a><\/li>\n<\/ul>\n<h2>\u4e60\u9898<\/h2>\n<ul>\n<li><a href=\"https:\/\/github.com\/lengyijun\/tarjan-kosaraju-why3-lean4\/blob\/main\/kosaraju-lean4\/Kosaraju\/Basic.lean\">\u9a8c\u8bc1\u4e86 scc \u7684 kosaraju \u56fe\u7b97\u6cd5<\/a><\/li>\n<li><a href=\"https:\/\/github.com\/AlexDuchnowski\/rubiks-cube\">\u9a8c\u8bc1\u9b54\u65b9\u7b97\u6cd5<\/a><\/li>\n<\/ul>\n<h2>\u7814\u7a76<\/h2>\n<ul>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2211.15864\">Peano: Learning Formal Mathematical Reasoning<\/a><\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2102.06203\">Proof Artifact Co-training for Theorem Proving with Language Models<\/a><\/li>\n<li><a href=\"https:\/\/arxiv.org\/abs\/2009.03393\">Generative Language Modeling for Automated Theorem Proving<\/a><\/li>\n<li><a href=\"https:\/\/openai.com\/index\/formal-math\/\">Solving (some) formal math olympiad problems<\/a><\/li>\n<li><a href=\"https:\/\/leandojo.org\/\">LeanDojo: Theorem Proving in Lean using Language Models<\/a><\/li>\n<li><a href=\"https:\/\/www.bilibili.com\/video\/BV1FJ4m1N74b\">\u5343\u91cc\u51b0\u5c01 &#8211; Canonical\u5b9a\u7406\u8bc1\u660e\u5668 -20240508-\uff08\u5185\u90e8\u62a5\u544a\uff0c\u975e\u516c\u5f00\u6f14\u8bb2\uff0c\u4ec5\u9650\u7231\u597d\u8005\u4ea4\u6d41\uff09<\/a><\/li>\n<\/ul>\n<h2>\u9879\u76ee<\/h2>\n<ul>\n<li><a href=\"https:\/\/xenaproject.wordpress.com\/what-is-the-xena-project\/\">Xena project<\/a><\/li>\n<li><a href=\"https:\/\/terrytao.wordpress.com\/2023\/11\/18\/formalizing-the-proof-of-pfr-in-lean4-using-blueprint-a-short-tour\/\">Formalizing the proof of PFR in Lean4 using Blueprint: a short tour<\/a><\/li>\n<li><a href=\"https:\/\/leanprover-community.github.io\/blog\/posts\/FLT-announcement\/\">The Fermat&#8217;s Last Theorem Project<\/a><\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>\u7531\u4e8e\u5404\u81ea\u4e0d\u540c\u7684\u539f\u56e0\uff0c\u53d1\u73b0\u5927\u5bb6\u8fd9\u4e2a\u5b66\u671f\u90fd\u5f00\u59cb\u5b66\u4e60\u8d77 Lean \u4e86\u8d77\u6765\uff0c\u6211\u4e5f\u4e0d\u80fd\u514d\u4fd7\u56e7\u3002L\u2203\u2200N \u4e00\u770b logo \u5c31\u5f88\u5e05\uff0c\u6709\u70b9 DUNE \u7684\u8bbe\u8ba1\u611f\u6709\u6ca1\u6709\uff1f \u611f\u89c9\u9996\u8981\u5de5\u4f5c\u662f\u5148\u590d\u4e60\u4e00\u4e0b Haskell\uff0c\u8fd9\u6837\u4e5f\u4e0d\u5fc5\u4e2d\u9014\u7ffb\u9605\u8bed\u6cd5\u624b\u518c\u3002\u663e\u7136 Lean4 \u4ece Haskell \u91cc\u501f\u9274\u4e86\u76f8\u5f53\u591a\u7684\u8bed\u6cd5\u548c\u8bbe\u8ba1\u601d\u60f3\uff0c\u8bf4\u6765\u60ed\u6127\uff0c\u867d\u7136\u6211\u4e4b\u524d\u8bd5\u56fe\u7528 Haskell \u5237\u5237\u9898\uff0c\u4f46\u662f\u603b\u662f\u611f\u89c9\u4e0d\u5f97\u8981\u9886\uff0c\u88ab\u590d\u6742\u5ea6\u5361\u7684\u6b7b\u6b7b\u7684\u56e7\u4e0d\u5f97\u4e0d\u4e2d\u9014\u5207\u56de cpp \u8279\u3002fingertree \u4ec0\u4e48\u7684\u4e5f\u770b\u7684\u4e91\u91cc\u96fe\u91cc\uff0c\u611f\u89c9\u8fd8\u662f\u6211\u7684\u59ff\u52bf\u6c34\u5e73\u4e0d\u591f\uff0c\u8fd8\u9700\u7279\u522b\u52aa\u529b\uff01 \u7136\u540e\u521d\u5b66 Lean \u6211\u662f\u5efa\u8bae\u5148\u770b Mathematics in Lean\uff0c\u672c\u4e66\u76f4\u63a5\u4f7f\u7528 mathlib\uff0c\u8ba9\u4f60\u4e0d\u5fc5\u8fc7\u65e9\u7684\u88ab\u7ec6\u8282\u529d\u9000\uff0c\u53c8\u53ef\u4ee5\u987a\u4fbf\u590d\u4e60\u4e00\u4e0b\u719f\u6089\u7684\u6570\u5b66\u77e5\u8bc6\uff08\u521d\u7b49\u6570\u8bba\u5979\u4e0d\u9999\u5417\uff0c\u5929\u5929\u5b66\u4ee3\u6570\u4eba\u90fd\u5b66\u50bb\u4e86\uff09\u3002\u800c\u4e14\u8fd8\u63d0\u4f9b\u5bf9\u5e94\u7684 Github \u4ed3\u5e93\uff0c\u53ef\u4ee5 step-by-step \u8fb9\u770b\u522b\u6539\u3002Lean \u4e0d\u80fd\u6ca1\u6709 mathlib\uff0c\u5c31\u50cf\u662f cpp \u4e0d\u80fd\u6ca1\u6709 std\uff0c\u897f\u65b9\u4e0d\u80fd\u6ca1\u6709\u8036\u8def\u6492\u51b7\uff1f \uff08\u76ee\u524d\u611f\u89c9\u8fd9\u8bed\u8a00\u9664\u4e86\u4f18\u5316\u4e0d\u884c\u54ea\u54ea\u90fd\u8fd8\u53ef\u4ee5\uff1f\uff09 \u518d\u7136\u540e\u611f\u89c9\u53ef\u4ee5\u8bd5\u8bd5\u5199\u70b9\u9898\u76ee\uff0c\u6bd4\u5982\u53ef\u4ee5\u8bd5\u8bd5\u5148\u8bc1\u660e\u9759\u6001\u76f4\u5f84\u7b97\u6cd5\uff1f \u5b66\u4e60 Lean (proof assistant), Wikipedia https:\/\/leanprover-community.github.io\/learn.html Lean Focused Research Organization Theorem Proving in Lean Mathematics in Lean Type [&hellip;]<\/p>\n","protected":false},"author":1,"featured_media":3286,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_jetpack_memberships_contains_paid_content":false,"footnotes":"","jetpack_publicize_message":"","jetpack_publicize_feature_enabled":true,"jetpack_social_post_already_shared":true,"jetpack_social_options":{"image_generator_settings":{"template":"highway","enabled":false}}},"categories":[1],"tags":[],"class_list":["post-3271","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-uncategorized"],"jetpack_publicize_connections":[],"jetpack_featured_media_url":"https:\/\/www.shuizilong.com\/house\/wp-content\/uploads\/2024\/05\/2024-05-12-02.41.35.jpg","jetpack_shortlink":"https:\/\/wp.me\/p2tdP7-QL","jetpack_sharing_enabled":true,"_links":{"self":[{"href":"https:\/\/www.shuizilong.com\/house\/wp-json\/wp\/v2\/posts\/3271","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.shuizilong.com\/house\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.shuizilong.com\/house\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.shuizilong.com\/house\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.shuizilong.com\/house\/wp-json\/wp\/v2\/comments?post=3271"}],"version-history":[{"count":21,"href":"https:\/\/www.shuizilong.com\/house\/wp-json\/wp\/v2\/posts\/3271\/revisions"}],"predecessor-version":[{"id":3295,"href":"https:\/\/www.shuizilong.com\/house\/wp-json\/wp\/v2\/posts\/3271\/revisions\/3295"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.shuizilong.com\/house\/wp-json\/wp\/v2\/media\/3286"}],"wp:attachment":[{"href":"https:\/\/www.shuizilong.com\/house\/wp-json\/wp\/v2\/media?parent=3271"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.shuizilong.com\/house\/wp-json\/wp\/v2\/categories?post=3271"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.shuizilong.com\/house\/wp-json\/wp\/v2\/tags?post=3271"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}