{"id":51224,"date":"2025-08-10T19:14:57","date_gmt":"2025-08-10T11:14:57","guid":{"rendered":"https:\/\/www.wsisp.com\/helps\/51224.html"},"modified":"2025-08-10T19:14:57","modified_gmt":"2025-08-10T11:14:57","slug":"%e7%aa%81%e7%a0%b4%e5%bd%a2%e5%bc%8f%e5%8c%96%e6%95%b0%e5%ad%a6%e8%af%81%e6%98%8e%e7%9a%84%e8%be%b9%e7%95%8c%ef%bc%9a%e5%ad%97%e8%8a%82%e8%b7%b3%e5%8a%a8delta-prover%e5%a6%82%e4%bd%95%e8%ae%a9","status":"publish","type":"post","link":"https:\/\/www.wsisp.com\/helps\/51224.html","title":{"rendered":"\u7a81\u7834\u5f62\u5f0f\u5316\u6570\u5b66\u8bc1\u660e\u7684\u8fb9\u754c\uff1a\u5b57\u8282\u8df3\u52a8Delta Prover\u5982\u4f55\u8ba9\u901a\u7528\u5927\u6a21\u578b\u5177\u5907\u9876\u5c16\u5b9a\u7406\u8bc1\u660e\u80fd\u529b"},"content":{"rendered":"<p>\u8bba\u6587\u540d\u79f0&#xff1a;Solving Formal Math Problems by Decomposition and Iterative Reflection<br \/>\n\u8bba\u6587\u5730\u5740&#xff1a;https:\/\/arxiv.org\/pdf\/2507.15225v1<\/p>\n<p>\u5728\u4eba\u5de5\u667a\u80fd\u9886\u57df&#xff0c;\u5f62\u5f0f\u5316\u6570\u5b66\u8bc1\u660e\u957f\u671f\u4ee5\u6765\u88ab\u89c6\u4e3a\u8861\u91cf\u673a\u5668\u63a8\u7406\u80fd\u529b\u7684&#034;\u73e0\u7a46\u6717\u739b\u5cf0&#034;\u3002\u4ece\u53e4\u5e0c\u814a\u51e0\u4f55\u516c\u7406\u5230\u73b0\u4ee3\u6570\u5b66\u7684\u590d\u6742\u5b9a\u7406&#xff0c;\u4eba\u7c7b\u4f9d\u9760\u903b\u8f91\u6f14\u7ece\u6784\u5efa\u4e86\u5b8f\u4f1f\u7684\u77e5\u8bc6\u5927\u53a6&#xff0c;\u800c\u8ba9\u673a\u5668\u638c\u63e1\u8fd9\u79cd\u7cbe\u5bc6\u63a8\u7406\u80fd\u529b\u4e00\u76f4\u662fAI\u7814\u7a76\u7684\u6838\u5fc3\u76ee\u6807\u3002\u8fd1\u671f&#xff0c;\u5b57\u8282\u8df3\u52a8Seed\u56e2\u961f\u53d1\u5e03\u7684Delta Prover\u6846\u67b6\u5728\u8fd9\u4e00\u9886\u57df\u53d6\u5f97\u4e86\u7a81\u7834\u6027\u8fdb\u5c55\u2014\u2014\u65e0\u9700\u4e13\u95e8\u8bad\u7ec3&#xff0c;\u4ec5\u901a\u8fc7\u901a\u7528\u5927\u6a21\u578b\u4e0eLean 4\u8bc1\u660e\u73af\u5883\u7684\u667a\u80fd\u534f\u4f5c&#xff0c;\u5c31\u5728miniF2F-test\u57fa\u51c6\u6d4b\u8bd5\u4e2d\u5b9e\u73b0\u4e8695.9%\u7684\u6210\u529f\u7387&#xff0c;\u8d85\u8d8a\u4e86\u6240\u6709\u9700\u8981\u6a21\u578b\u4e13\u95e8\u5316\u7684\u73b0\u6709\u65b9\u6cd5\u3002\u8fd9\u4e00\u6210\u679c\u4e0d\u4ec5\u5237\u65b0\u4e86\u81ea\u52a8\u5b9a\u7406\u8bc1\u660e\u7684\u6027\u80fd\u7eaa\u5f55&#xff0c;\u66f4\u63ed\u793a\u4e86\u901a\u7528\u5927\u6a21\u578b\u5728\u6709\u6548\u5f15\u5bfc\u4e0b\u8574\u85cf\u7684\u5de8\u5927\u6f5c\u80fd\u3002\u672c\u6587\u5c06\u6df1\u5165\u89e3\u6790Delta Prover\u7684\u521b\u65b0\u67b6\u6784\u3001\u6280\u672f\u7ec6\u8282\u4e0e\u5b9e\u9a8c\u6210\u679c&#xff0c;\u63a2\u8ba8\u8fd9\u4e00\u7a81\u7834\u5bf9AI\u63a8\u7406\u548c\u6570\u5b66\u7814\u7a76\u7684\u6df1\u8fdc\u5f71\u54cd\u3002<\/p>\n<h3>\u5f62\u5f0f\u5316\u6570\u5b66\u8bc1\u660e&#xff1a;AI\u63a8\u7406\u7684\u7ec8\u6781\u6311\u6218<\/h3>\n<p>\u6570\u5b66\u8bc1\u660e\u7684\u5f62\u5f0f\u5316\u8868\u8fbe\u4e0e\u9a8c\u8bc1\u662f\u4eba\u5de5\u667a\u80fd\u9886\u57df\u7684\u91cd\u8981\u524d\u6cbf\u3002\u4e0e\u81ea\u7136\u8bed\u8a00\u6570\u5b66\u63a8\u7406\u4e0d\u540c&#xff0c;\u5f62\u5f0f\u5316\u8bc1\u660e\u8981\u6c42\u6bcf\u4e00\u6b65\u903b\u8f91\u6f14\u7ece\u90fd\u5fc5\u987b\u4e25\u683c\u9075\u5faa\u5f62\u5f0f\u8bed\u8a00\u7684\u8bed\u6cd5\u89c4\u5219\u548c\u516c\u7406\u7cfb\u7edf&#xff0c;\u786e\u4fdd\u7edd\u5bf9\u6b63\u786e\u6027\u3002\u8fd9\u79cd\u4e25\u683c\u6027\u4f7f\u5f97\u5f62\u5f0f\u5316\u8bc1\u660e\u6210\u4e3a\u9a8c\u8bc1\u590d\u6742\u7cfb\u7edf&#xff08;\u4ece\u8f6f\u4ef6\u7b97\u6cd5\u5230\u786c\u4ef6\u8bbe\u8ba1&#xff09;\u7684\u7406\u60f3\u5de5\u5177&#xff0c;\u4f46\u540c\u65f6\u4e5f\u4e3aAI\u7cfb\u7edf\u5e26\u6765\u4e86\u72ec\u7279\u6311\u6218\u3002<\/p>\n<p>\u5f53\u4ee3\u5f62\u5f0f\u5316\u8bc1\u660e\u7cfb\u7edf\u5982Lean\u3001Isabelle\u548cCoq\u5df2\u7ecf\u6210\u4e3a\u6570\u5b66\u5bb6\u548c\u8ba1\u7b97\u673a\u79d1\u5b66\u5bb6\u7684\u91cd\u8981\u5de5\u5177\u3002\u4ee5Lean 4\u4e3a\u4f8b&#xff0c;\u5b83\u4e0d\u4ec5\u662f\u4e00\u4e2a\u5b9a\u7406\u8bc1\u660e\u5668&#xff0c;\u8fd8\u662f\u4e00\u79cd\u51fd\u6570\u5f0f\u7f16\u7a0b\u8bed\u8a00&#xff0c;\u5141\u8bb8\u7528\u6237\u4ee5\u7cbe\u786e\u7684\u5f62\u5f0f\u5316\u8bed\u8a00\u5b9a\u4e49\u6570\u5b66\u6982\u5ff5\u5e76\u6784\u5efa\u8bc1\u660e\u3002\u8fd9\u4e9b\u7cfb\u7edf\u7684\u6838\u5fc3\u4f18\u52bf\u5728\u4e8e\u5176\u81ea\u52a8\u9a8c\u8bc1\u80fd\u529b\u2014\u2014\u901a\u8fc7\u5185\u7f6e\u7684&#034;\u5185\u6838&#034;&#xff08;kernel&#xff09;\u53ef\u4ee5\u673a\u68b0\u5730\u68c0\u67e5\u6bcf\u4e00\u6b65\u63a8\u7406\u662f\u5426\u7b26\u5408\u903b\u8f91\u89c4\u5219&#xff0c;\u4ece\u6839\u672c\u4e0a\u6d88\u9664\u4e86\u81ea\u7136\u8bed\u8a00\u8bc1\u660e\u4e2d\u5e38\u89c1\u7684\u6a21\u7cca\u6027\u548c\u9519\u8bef\u9690\u60a3\u3002<\/p>\n<p>\u7136\u800c&#xff0c;\u8ba9AI\u7cfb\u7edf\u638c\u63e1\u5f62\u5f0f\u5316\u8bc1\u660e\u6280\u672f\u9762\u4e34\u53cc\u91cd\u56f0\u5883\u3002\u9996\u5148&#xff0c;\u5f62\u5f0f\u5316\u8bed\u8a00\u4e0e\u901a\u7528\u7f16\u7a0b\u8bed\u8a00\u5b58\u5728\u663e\u8457\u5dee\u5f02&#xff0c;\u5176\u72ec\u7279\u7684\u8bed\u6cd5\u7ed3\u6784\u548c\u903b\u8f91\u8303\u5f0f\u4f7f\u5f97\u4e3b\u8981\u8bad\u7ec3\u4e8e\u901a\u7528\u4ee3\u7801\u7684\u5927\u6a21\u578b\u96be\u4ee5\u76f4\u63a5\u751f\u6210\u6b63\u786e\u7684\u5f62\u5f0f\u5316\u8bc1\u660e\u4ee3\u7801\u3002\u6570\u636e\u7a00\u7f3a\u6027\u52a0\u5267\u4e86\u8fd9\u4e00\u95ee\u9898&#xff1a;\u76ee\u524d\u6700\u5927\u7684Lean 4\u4ee3\u7801\u5e93LEAN-GitHub\u4ec5\u5305\u542b0.13B tokens&#xff0c;\u4ec5\u5360\u5178\u578b\u4ee3\u7801\u8bed\u6599\u5e93\u76840.1%&#xff0c;\u5bfc\u81f4\u901a\u7528\u5927\u6a21\u578b\u5728\u5f62\u5f0f\u5316\u8bed\u8a00\u4e0a\u7684\u719f\u7ec3\u5ea6\u4e25\u91cd\u4e0d\u8db3\u3002<\/p>\n<p>\u5176\u6b21&#xff0c;\u73b0\u6709\u65b9\u6cd5\u901a\u5e38\u4f9d\u8d56\u4e8e\u4e13\u95e8\u8bad\u7ec3\u7684\u6a21\u578b&#xff0c;\u8fd9\u9700\u8981\u5927\u91cf\u9ad8\u8d28\u91cf\u7684\u6807\u6ce8\u6570\u636e\u548c\u5de8\u989d\u8ba1\u7b97\u8d44\u6e90\u3002\u83b7\u53d6\u5f62\u5f0f\u5316\u8bc1\u660e\u6570\u636e\u5c24\u5176\u56f0\u96be&#xff0c;\u56e0\u4e3a\u5b83\u8981\u6c42\u6807\u6ce8\u8005\u540c\u65f6\u5177\u5907\u9ad8\u7ea7\u6570\u5b66\u77e5\u8bc6\u548c\u7279\u5b9a\u5f62\u5f0f\u5316\u8bed\u8a00\u7684\u4e13\u4e1a\u6280\u80fd\u3002\u8fd9\u79cd\u6570\u636e\u74f6\u9888\u4f7f\u5f97\u4e13\u7528\u6a21\u578b\u7684\u5f00\u53d1\u6210\u672c\u9ad8\u6602&#xff0c;\u4e14\u96be\u4ee5\u63a8\u5e7f\u5230\u66f4\u5e7f\u6cdb\u7684\u6570\u5b66\u9886\u57df\u3002<\/p>\n<p>\u4f20\u7edf\u7684\u5f62\u5f0f\u5316\u5b9a\u7406\u8bc1\u660e\u65b9\u6cd5\u5b58\u5728\u660e\u663e\u5c40\u9650\u6027\u3002\u65e9\u671f\u5de5\u4f5c\u5982GPT-f\u5c55\u793a\u4e86\u751f\u6210\u5f0f\u9884\u8bad\u7ec3\u5728\u5b9a\u7406\u8bc1\u660e\u4e2d\u7684\u6f5c\u529b&#xff0c;\u4f46\u6027\u80fd\u53d7\u9650&#xff1b;\u540e\u7eed\u65b9\u6cd5\u5982DeepSeek Prover\u548cKimina Prover\u901a\u8fc7\u5927\u89c4\u6a21\u5fae\u8c03\u5b9e\u73b0\u4e86\u6027\u80fd\u63d0\u5347&#xff0c;\u4f46\u9700\u8981\u6301\u7eed\u7684\u4e13\u4e1a\u6570\u636e\u6807\u6ce8\u548c\u8ba1\u7b97\u6295\u5165\u3002\u66f4\u91cd\u8981\u7684\u662f&#xff0c;\u8fd9\u4e9b\u65b9\u6cd5\u5927\u591a\u91c7\u7528\u5e76\u884c\u91c7\u6837\u7b56\u7565&#xff08;Best-of-N&#xff09;&#xff0c;\u901a\u8fc7\u751f\u6210\u591a\u4e2a\u72ec\u7acb\u7684\u8bc1\u660e\u5c1d\u8bd5\u5e76\u9009\u62e9\u6709\u6548\u7684\u7ed3\u679c&#xff0c;\u4f46\u8fd9\u79cd\u65b9\u5f0f\u65e0\u6cd5\u5145\u5206\u5229\u7528\u5927\u6a21\u578b\u7684\u63a8\u7406\u548c\u53cd\u601d\u80fd\u529b&#xff0c;\u5bfc\u81f4\u6d4b\u8bd5\u65f6\u7684\u6548\u7387\u548c\u6269\u5c55\u6027\u4e0d\u4f73\u3002<\/p>\n<p>\u6b63\u662f\u5728\u8fd9\u4e00\u80cc\u666f\u4e0b&#xff0c;\u5b57\u8282\u8df3\u52a8Seed\u56e2\u961f\u63d0\u51fa\u4e86Delta Prover\u6846\u67b6&#xff0c;\u5f00\u8f9f\u4e86\u4e00\u6761\u57fa\u4e8e\u901a\u7528\u5927\u6a21\u578b\u6784\u5efa\u9ad8\u6548\u5f62\u5f0f\u5316\u8bc1\u660e\u7cfb\u7edf\u7684\u65b0\u8def\u5f84\u3002\u4ed6\u4eec\u7684\u6838\u5fc3 insight \u662f&#xff1a;\u901a\u7528\u5927\u6a21\u578b\u5df2\u7ecf\u5177\u5907\u5f3a\u5927\u7684\u63a8\u7406\u548c\u53cd\u601d\u80fd\u529b&#xff0c;\u5173\u952e\u5728\u4e8e\u8bbe\u8ba1\u6709\u6548\u7684\u6846\u67b6\u6765\u5f15\u5bfc\u8fd9\u4e9b\u80fd\u529b\u5728\u5f62\u5f0f\u5316\u8bc1\u660e\u73af\u5883\u4e2d\u53d1\u6325\u4f5c\u7528&#xff0c;\u800c\u975e\u901a\u8fc7\u6602\u8d35\u7684\u4e13\u95e8\u8bad\u7ec3\u6765&#034;\u786c\u7f16\u7801&#034;\u5f62\u5f0f\u5316\u63a8\u7406\u80fd\u529b\u3002<\/p>\n<h3>Delta Prover\u67b6\u6784&#xff1a;\u901a\u7528\u5927\u6a21\u578b\u7684\u5f62\u5f0f\u5316\u63a8\u7406\u8d4b\u80fd\u6846\u67b6<\/h3>\n<p>Delta Prover\u7684\u9769\u547d\u6027\u7a81\u7834\u6e90\u4e8e\u5176\u521b\u65b0\u7684\u4ee3\u7406\u5f0f\u67b6\u6784&#xff08;agent-based framework&#xff09;&#xff0c;\u8be5\u67b6\u6784\u5de7\u5999\u5730\u534f\u8c03\u901a\u7528\u5927\u6a21\u578b\u4e0eLean 4\u8bc1\u660e\u73af\u5883\u7684\u4ea4\u4e92&#xff0c;\u65e0\u9700\u4efb\u4f55\u6a21\u578b\u5fae\u8c03\u5373\u53ef\u5b9e\u73b0\u9876\u5c16\u7684\u5f62\u5f0f\u5316\u8bc1\u660e\u80fd\u529b\u3002\u8fd9\u4e00\u67b6\u6784\u7684\u6838\u5fc3\u662f\u5c06\u5927\u6a21\u578b\u4ece\u88ab\u52a8\u7684\u8bc1\u660e\u751f\u6210\u5668\u8f6c\u53d8\u4e3a\u4e3b\u52a8\u7684\u63a8\u7406\u4ee3\u7406&#xff0c;\u901a\u8fc7\u53cd\u601d\u548c\u8fed\u4ee3\u4f18\u5316\u8fc7\u7a0b\u6784\u5efa\u6b63\u786e\u7684\u5f62\u5f0f\u5316\u8bc1\u660e\u3002<\/p>\n<h4>\u6574\u4f53\u6846\u67b6\u8bbe\u8ba1<\/h4>\n<p>Delta Prover\u7684\u67b6\u6784\u56f4\u7ed5\u4e24\u4e2a\u76f8\u4e92\u4f9d\u5b58\u7684\u6838\u5fc3\u7ec4\u4ef6\u6784\u5efa&#xff1a;\u53cd\u5c04\u5f0f\u5206\u89e3&#xff08;reflective decomposition&#xff09;\u4e0e\u8fed\u4ee3\u5f0f\u8bc1\u660e\u4fee\u590d&#xff08;iterative proof repair&#xff09;\u7684\u7b97\u6cd5\u6846\u67b6&#xff0c;\u4ee5\u53ca\u57fa\u4e8eLean 4\u6784\u5efa\u7684\u4e13\u7528\u9886\u57df\u7279\u5b9a\u8bed\u8a00&#xff08;DSL&#xff09;\u3002\u8fd9\u79cd\u8bbe\u8ba1\u4f7f\u7cfb\u7edf\u80fd\u591f\u5c06\u590d\u6742\u5b9a\u7406\u5206\u89e3\u4e3a\u53ef\u7ba1\u7406\u7684\u5b50\u95ee\u9898&#xff0c;\u5e76\u901a\u8fc7\u6301\u7eed\u53cd\u9988\u9010\u6b65\u4fee\u6b63\u8bc1\u660e\u9519\u8bef&#xff0c;\u6700\u7ec8\u6574\u5408\u4e3a\u5b8c\u6574\u7684\u5f62\u5f0f\u5316\u8bc1\u660e\u3002<\/p>\n<p><img decoding=\"async\" src=\"https:\/\/www.wsisp.com\/helps\/wp-content\/uploads\/2025\/08\/20250810111441-68987f210bf85.png\" alt=\"\u5728\u8fd9\u91cc\u63d2\u5165\u56fe\u7247\u63cf\u8ff0\" \/><\/p>\n<p>\u56fe1&#xff1a;Delta Prover\u7684\u6838\u5fc3\u7ec4\u4ef6\u5305\u62ec\u53cd\u5c04\u5f0f\u5206\u89e3\u4e0e\u8fed\u4ee3\u5f0f\u8bc1\u660e\u4fee\u590d\u8fc7\u7a0b&#xff0c;\u4e8c\u8005\u901a\u8fc7\u4e13\u7528DSL\u534f\u540c\u5de5\u4f5c<\/p>\n<p>\u7cfb\u7edf\u7684\u5de5\u4f5c\u6d41\u7a0b\u4f53\u73b0\u4e86\u660e\u663e\u7684&#034;\u4ee3\u7406&#034;\u7279\u6027&#xff1a;\u9762\u5bf9\u4e00\u4e2a\u5f62\u5f0f\u5316\u5b9a\u7406&#xff0c;Delta Prover\u9996\u5148\u5c1d\u8bd5\u76f4\u63a5\u8bc1\u660e&#xff1b;\u82e5\u76f4\u63a5\u8bc1\u660e\u5931\u8d25&#xff0c;\u5219\u542f\u52a8\u53cd\u5c04\u5f0f\u5206\u89e3\u8fc7\u7a0b&#xff0c;\u5c06\u539f\u95ee\u9898\u62c6\u89e3\u4e3a\u4e00\u7cfb\u5217\u5b50\u95ee\u9898&#xff1b;\u6bcf\u4e2a\u5b50\u95ee\u9898\u901a\u8fc7\u8fed\u4ee3\u5f0f\u8bc1\u660e\u4fee\u590d\u673a\u5236\u72ec\u7acb\u89e3\u51b3&#xff1b;\u6700\u540e&#xff0c;\u7cfb\u7edf\u5c06\u6240\u6709\u5b50\u95ee\u9898\u7684\u8bc1\u660e\u81ea\u52a8\u6574\u5408\u4e3a\u539f\u5b9a\u7406\u7684\u5b8c\u6574\u8bc1\u660e\u3002\u8fd9\u79cd\u5206\u800c\u6cbb\u4e4b\u7684\u7b56\u7565\u5927\u5e45\u964d\u4f4e\u4e86\u590d\u6742\u5b9a\u7406\u7684\u8bc1\u660e\u96be\u5ea6&#xff0c;\u540c\u65f6\u5145\u5206\u5229\u7528\u4e86\u5927\u6a21\u578b\u7684\u95ee\u9898\u5206\u89e3\u80fd\u529b\u3002<\/p>\n<h4>\u8fed\u4ee3\u5f0f\u8bc1\u660e\u4fee\u590d&#xff1a;\u9519\u8bef\u9a71\u52a8\u7684\u7cbe\u7ec6\u5316\u4f18\u5316<\/h4>\n<p><img decoding=\"async\" src=\"https:\/\/www.wsisp.com\/helps\/wp-content\/uploads\/2025\/08\/20250810111443-68987f232eca6.png\" alt=\"\u5728\u8fd9\u91cc\u63d2\u5165\u56fe\u7247\u63cf\u8ff0\" \/><\/p>\n<p>\u8fed\u4ee3\u5f0f\u8bc1\u660e\u4fee\u590d\u662fDelta Prover\u7684\u57fa\u7840\u673a\u5236&#xff0c;\u65e8\u5728\u901a\u8fc7\u6301\u7eed\u53cd\u9988\u548c\u4fee\u6b63\u6765\u5b8c\u5584\u8bc1\u660e\u5c1d\u8bd5\u3002\u4e0e\u4f20\u7edf\u7684\u4e00\u6b21\u6027\u751f\u6210\u7b56\u7565\u4e0d\u540c&#xff0c;\u8fd9\u4e00\u673a\u5236\u5efa\u7acb\u4e86\u5927\u6a21\u578b\u4e0eLean 4\u73af\u5883\u4e4b\u95f4\u7684\u7d27\u5bc6\u53cd\u9988\u5faa\u73af&#xff0c;\u4f7f\u7cfb\u7edf\u80fd\u591f\u4ece\u9519\u8bef\u4e2d\u5b66\u4e60\u5e76\u9010\u6b65\u6539\u8fdb\u8bc1\u660e\u3002<\/p>\n<p>\u8be5\u8fc7\u7a0b\u7684\u5de5\u4f5c\u539f\u7406\u53ef\u6982\u62ec\u4e3a\u4ee5\u4e0b\u6b65\u9aa4&#xff1a;<\/p>\n<li>\n<p>\u521d\u59cb\u8bc1\u660e\u751f\u6210&#xff1a;\u7ed9\u5b9a\u5f62\u5f0f\u5316\u547d\u9898&#xff0c;\u5927\u6a21\u578b\u751f\u6210\u521d\u59cb\u7684\u8bc1\u660e\u5c1d\u8bd5\u3002\u4e3a\u63d0\u9ad8\u521d\u59cb\u8d28\u91cf&#xff0c;\u7cfb\u7edf\u63d0\u4f9b\u4e86\u8be6\u7ec6\u7684\u6307\u5bfc&#xff0c;\u5305\u62ecLean 4\u7684\u683c\u5f0f\u7ea6\u5b9a&#xff08;\u5982rcases\u548ccases\u7b49\u6218\u672f\u7684\u6b63\u786e\u4f7f\u7528&#xff09;\u3001Mathlib\u5e93\u4e2d\u5f3a\u5927\u6218\u672f&#xff08;\u5982linarith\u3001ring\u548comega&#xff09;\u7684\u6587\u6863\u8bf4\u660e&#xff0c;\u4ee5\u53ca\u4e25\u683c\u7684Lean 4\u8bed\u6cd5\u89c4\u8303&#xff08;\u907f\u514d\u751f\u6210\u4e0eLean 3\u517c\u5bb9\u7684\u4ee3\u7801&#xff09;\u3002<\/p>\n<\/li>\n<li>\n<p>\u9a8c\u8bc1\u4e0e\u9519\u8bef\u8bca\u65ad&#xff1a;Lean 4\u5185\u6838\u9a8c\u8bc1\u521d\u59cb\u8bc1\u660e&#xff0c;\u82e5\u5b58\u5728\u9519\u8bef\u5219\u8fd4\u56de\u8be6\u7ec6\u7684\u9519\u8bef\u4fe1\u606f&#xff0c;\u5305\u62ec\u9519\u8bef\u4f4d\u7f6e\u3001\u7c7b\u578b\u53ca\u53ef\u80fd\u7684\u4fee\u590d\u5efa\u8bae\u3002\u8fd9\u4e9b\u8bca\u65ad\u4fe1\u606f\u6210\u4e3a\u540e\u7eed\u4fee\u6b63\u7684\u5173\u952e\u4f9d\u636e\u3002<\/p>\n<\/li>\n<li>\n<p>\u589e\u5f3a\u53cd\u9988\u4e0e\u8bc1\u660e\u4fee\u6b63&#xff1a;\u5f53\u8bc1\u660e\u5c1d\u8bd5\u5931\u8d25\u65f6&#xff0c;\u7cfb\u7edf\u6784\u5efa\u5305\u542b\u591a\u7ef4\u5ea6\u4fe1\u606f\u7684\u589e\u5f3a\u63d0\u793a&#xff1a;<\/p>\n<ul>\n<li>\u5931\u8d25\u7684\u8bc1\u660e\u4ee3\u7801\u672c\u8eab<\/li>\n<li>Lean 4\u5185\u6838\u8fd4\u56de\u7684\u5b8c\u6574\u9519\u8bef\u6d88\u606f\u548c\u6218\u672f\u72b6\u6001<\/li>\n<li>\u57fa\u4e8e\u9519\u8bef\u5185\u5bb9\u68c0\u7d22\u7684\u76f8\u5173\u5b9a\u7406\u548c\u5b9a\u4e49&#xff08;\u89e3\u51b3\u5927\u6a21\u578b\u5bf9Mathlib\u5e93\u4e2d\u5177\u4f53\u6807\u8bc6\u7b26\u8bb0\u5fc6\u4e0d\u51c6\u786e\u7684\u95ee\u9898&#xff09;<\/li>\n<\/ul>\n<\/li>\n<li>\n<p>\u8fed\u4ee3\u4f18\u5316&#xff1a;\u5927\u6a21\u578b\u57fa\u4e8e\u589e\u5f3a\u53cd\u9988\u751f\u6210\u4fee\u6b63\u540e\u7684\u8bc1\u660e&#xff0c;\u8fd9\u4e00\u8fc7\u7a0b\u53ef\u91cd\u590d\u591a\u6b21\u76f4\u5230\u8bc1\u660e\u6210\u529f\u6216\u8fbe\u5230\u6700\u5927\u8fed\u4ee3\u6b21\u6570\u3002<\/p>\n<\/li>\n<p>\u7b97\u6cd51\u5c55\u793a\u4e86\u8fed\u4ee3\u5f0f\u8bc1\u660e\u4fee\u590d\u7684\u4f2a\u4ee3\u7801\u5b9e\u73b0\u3002\u8be5\u673a\u5236\u7684\u6838\u5fc3\u4f18\u52bf\u5728\u4e8e\u5176\u5229\u7528\u5927\u6a21\u578b\u53cd\u601d\u80fd\u529b\u8fdb\u884c\u9519\u8bef\u4fee\u6b63\u7684\u80fd\u529b&#xff0c;\u901a\u8fc7\u805a\u7126\u4e8e\u9519\u8bef\u70b9\u800c\u975e\u91cd\u65b0\u751f\u6210\u6574\u4e2a\u8bc1\u660e&#xff0c;\u663e\u8457\u63d0\u9ad8\u4e86\u8bc1\u660e\u6548\u7387\u3002\u5b9e\u9a8c\u6570\u636e\u8868\u660e&#xff0c;\u5728\u56fa\u5b9a\u9884\u7b97\u4e0b&#xff0c;\u589e\u52a0\u4fee\u590d\u6b21\u6570&#xff08;n&#xff09;\u6bd4\u589e\u52a0\u72ec\u7acb\u5c1d\u8bd5\u6b21\u6570&#xff08;m&#xff09;\u80fd\u5e26\u6765\u66f4\u9ad8\u7684\u6210\u529f\u7387&#xff0c;\u8fd9\u9a8c\u8bc1\u4e86\u53cd\u601d\u80fd\u529b\u5728\u5f62\u5f0f\u5316\u8bc1\u660e\u4e2d\u7684\u5173\u952e\u4ef7\u503c\u3002<\/p>\n<h4>\u53cd\u5c04\u5f0f\u5206\u89e3&#xff1a;\u590d\u6742\u95ee\u9898\u7684\u7ed3\u6784\u5316\u62c6\u89e3<\/h4>\n<p><img decoding=\"async\" src=\"https:\/\/www.wsisp.com\/helps\/wp-content\/uploads\/2025\/08\/20250810111444-68987f2483603.png\" alt=\"\u5728\u8fd9\u91cc\u63d2\u5165\u56fe\u7247\u63cf\u8ff0\" \/><\/p>\n<p>\u5bf9\u4e8e\u76f4\u63a5\u8bc1\u660e\u96be\u4ee5\u89e3\u51b3\u7684\u590d\u6742\u5b9a\u7406&#xff0c;Delta Prover\u5f15\u5165\u4e86\u53cd\u5c04\u5f0f\u5206\u89e3\u673a\u5236&#xff0c;\u5c06\u539f\u95ee\u9898\u7cfb\u7edf\u5730\u5206\u89e3\u4e3a\u66f4\u7b80\u5355\u7684\u5b50\u95ee\u9898&#xff0c;\u901a\u8fc7\u89e3\u51b3\u5b50\u95ee\u9898\u6765\u95f4\u63a5\u6784\u5efa\u539f\u5b9a\u7406\u7684\u8bc1\u660e\u3002\u8fd9\u4e00\u8fc7\u7a0b\u53d7\u5230\u4eba\u7c7b\u6570\u5b66\u5bb6\u8bc1\u660e\u590d\u6742\u5b9a\u7406\u65f6\u5e38\u7528\u7b56\u7565\u7684\u542f\u53d1&#xff1a;\u5c06\u5927\u95ee\u9898\u5206\u89e3\u4e3a\u5f15\u7406&#xff0c;\u9010\u4e00\u8bc1\u660e\u540e\u518d\u6574\u5408\u3002<\/p>\n<p>\u53cd\u5c04\u5f0f\u5206\u89e3\u7684\u5b9e\u73b0\u5305\u542b\u4e09\u4e2a\u5173\u952e\u6b65\u9aa4&#xff1a;<\/p>\n<li>\n<p>\u975e\u5f62\u5f0f\u5316\u8bc1\u660e\u89c4\u5212&#xff1a;\u5927\u6a21\u578b\u9996\u5148\u751f\u6210\u539f\u5b9a\u7406\u7684\u81ea\u7136\u8bed\u8a00\u8bc1\u660e\u6982\u8981&#xff0c;\u4ee5 step-by-step \u7684\u5f62\u5f0f\u63cf\u8ff0\u8bc1\u660e\u601d\u8def\u3002\u8fd9\u4e00\u6b65\u9aa4\u5e2e\u52a9\u5927\u6a21\u578b\u7406\u6e05\u8bc1\u660e\u7ed3\u6784&#xff0c;\u4e3a\u540e\u7eed\u7684\u5f62\u5f0f\u5316\u5206\u89e3\u5960\u5b9a\u57fa\u7840\u3002<\/p>\n<\/li>\n<li>\n<p>\u5f62\u5f0f\u5316\u8bc1\u660e\u8349\u56fe\u751f\u6210&#xff1a;\u57fa\u4e8e\u81ea\u7136\u8bed\u8a00\u8bc1\u660e\u6982\u8981&#xff0c;\u5927\u6a21\u578b\u4f7f\u7528\u4e13\u7528DSL\u751f\u6210\u5f62\u5f0f\u5316\u8bc1\u660e\u8349\u56fe\u3002\u7cfb\u7edf\u901a\u8fc7\u63d0\u4f9bDSL\u8bed\u6cd5\u793a\u4f8b\u548c\u5e38\u89c1\u5f62\u5f0f\u5316\u9677\u9631&#xff08;\u5982\u9690\u5f0f\u5047\u8bbe\u548c\u91cf\u8bcd\u8303\u56f4\u9519\u8bef&#xff09;\u7684\u8b66\u793a&#xff0c;\u5f15\u5bfc\u5927\u6a21\u578b\u751f\u6210\u51c6\u786e\u7684\u5f62\u5f0f\u5316\u7ed3\u6784\u3002<\/p>\n<\/li>\n<li>\n<p>\u5b50\u95ee\u9898\u63d0\u53d6\u4e0e\u6c42\u89e3&#xff1a;DSL\u901a\u8fc7show\u2026by\u6218\u672f\u81ea\u52a8\u4ece\u5f62\u5f0f\u5316\u8349\u56fe\u4e2d\u63d0\u53d6\u5b50\u95ee\u9898&#xff0c;\u6bcf\u4e2a\u5b50\u95ee\u9898\u90fd\u901a\u8fc7\u8fed\u4ee3\u5f0f\u8bc1\u660e\u4fee\u590d\u673a\u5236\u72ec\u7acb\u6c42\u89e3\u3002\u82e5\u67d0\u4e9b\u5b50\u95ee\u9898\u65e0\u6cd5\u89e3\u51b3&#xff0c;\u7cfb\u7edf\u5c06\u672a\u89e3\u51b3\u7684\u5b50\u95ee\u9898\u5217\u8868\u53cd\u9988\u7ed9\u5927\u6a21\u578b&#xff0c;\u6307\u5bfc\u5176\u8c03\u6574\u5206\u89e3\u7b56\u7565\u5e76\u91cd\u65b0\u751f\u6210\u8bc1\u660e\u8349\u56fe\u3002<\/p>\n<\/li>\n<p>\u7b97\u6cd52\u8be6\u7ec6\u63cf\u8ff0\u4e86\u8fd9\u4e00\u8fc7\u7a0b\u3002\u53cd\u5c04\u5f0f\u5206\u89e3\u7684\u6838\u5fc3\u521b\u65b0\u5728\u4e8e\u5176&#034;\u53cd\u5c04&#034;\u7279\u6027\u2014\u2014\u7cfb\u7edf\u4e0d\u4ec5\u5206\u89e3\u95ee\u9898&#xff0c;\u8fd8\u80fd\u6839\u636e\u5b50\u95ee\u9898\u7684\u6c42\u89e3\u60c5\u51b5\u53cd\u601d\u5206\u89e3\u7b56\u7565\u7684\u6709\u6548\u6027\u5e76\u8fdb\u884c\u52a8\u6001\u8c03\u6574\u3002\u8fd9\u79cd\u81ea\u9002\u5e94\u80fd\u529b\u4f7f\u7cfb\u7edf\u80fd\u591f\u5904\u7406\u4f20\u7edf\u5206\u89e3\u65b9\u6cd5\u96be\u4ee5\u5e94\u5bf9\u7684\u590d\u6742\u95ee\u9898\u3002<\/p>\n<h4>\u9886\u57df\u7279\u5b9a\u8bed\u8a00&#xff08;DSL&#xff09;&#xff1a;\u5b50\u95ee\u9898\u7ba1\u7406\u7684\u6280\u672f\u652f\u67f1<\/h4>\n<p><img decoding=\"async\" src=\"https:\/\/www.wsisp.com\/helps\/wp-content\/uploads\/2025\/08\/20250810111445-68987f2568063.png\" alt=\"\u5728\u8fd9\u91cc\u63d2\u5165\u56fe\u7247\u63cf\u8ff0\" \/><\/p>\n<p>\u4e3a\u652f\u6301\u53cd\u5c04\u5f0f\u5206\u89e3\u548c\u8bc1\u660e\u6574\u5408&#xff0c;Delta Prover\u6784\u5efa\u4e86\u57fa\u4e8eLean 4\u5143\u7f16\u7a0b\u80fd\u529b\u7684\u4e13\u7528DSL\u3002\u8be5DSL\u5728Lean 4\u7684TacticM\u57fa\u7840\u4e0a\u5f15\u5165\u4e86PlayM monad\u5c42&#xff0c;\u7528\u4e8e\u8bb0\u5f55\u548c\u7ba1\u7406\u4e2d\u95f4\u8bc1\u660e\u72b6\u6001&#xff0c;\u6700\u7ec8\u901a\u8fc7Lean 4\u7684delaborator\u8f6c\u6362\u4e3a\u6709\u6548\u7684Lean 4\u8bc1\u660e\u811a\u672c\u3002<\/p>\n<p>DSL\u63d0\u4f9b\u4e86\u56db\u4e2a\u5173\u952e\u6218\u672f&#xff0c;\u652f\u6491\u8d77\u5b8c\u6574\u7684\u5b50\u95ee\u9898\u7ba1\u7406\u751f\u547d\u5468\u671f&#xff1a;<\/p>\n<ul>\n<li>Suppose\u6218\u672f&#xff1a;\u7528\u4e8e\u5f15\u5165\u65b0\u7684\u5047\u8bbe\u5230\u8bc1\u660e\u73af\u5883\u4e2d&#xff0c;\u5141\u8bb8\u5047\u8bbe\u4efb\u610fLean 4\u7c7b\u578b\u4f5c\u4e3a\u524d\u63d0\u800c\u65e0\u9700\u6307\u5b9a\u5177\u4f53\u503c\u3002<\/li>\n<li>Define\u6218\u672f&#xff1a;\u652f\u6301\u5f15\u5165\u4efb\u610fLean 4\u8868\u8fbe\u5f0f\u5e76\u81ea\u52a8\u63a8\u65ad\u5176\u7c7b\u578b&#xff0c;\u4f8b\u5982\u5b9a\u4e49\u4ece\u6574\u6570\u5230\u6574\u6570\u7684\u51fd\u6570\u6216\u81ea\u7136\u6570\u4e0a\u7684\u6709\u9650\u96c6\u3002<\/li>\n<li>ShowBy\u6218\u672f&#xff1a;\u5728PlayM\u548cTacticM\u4e4b\u95f4\u5efa\u7acb\u63a5\u53e3&#xff0c;\u5141\u8bb8\u660e\u786e\u63d0\u51fa\u5b50\u76ee\u6807\u5e76\u8bb0\u5f55\u5176\u8bc1\u660e\u8fc7\u7a0b&#xff0c;\u4e3a\u540e\u7eed\u6574\u5408\u505a\u51c6\u5907\u3002<\/li>\n<li>Conclude\u6218\u672f&#xff1a;\u8d1f\u8d23\u8bc1\u660e\u6574\u5408&#xff0c;\u5229\u7528\u8bb0\u5f55\u7684\u6240\u6709\u5b50\u95ee\u9898\u8bc1\u660e\u548c\u4f9d\u8d56\u5173\u7cfb\u56fe&#xff0c;\u751f\u6210\u539f\u5b9a\u7406\u7684\u5b8c\u6574\u8bc1\u660e\u3002<\/li>\n<\/ul>\n<p>\u56fe3\u5c55\u793a\u4e86DSL\u5982\u4f55\u652f\u6301\u4ece\u95ee\u9898\u5206\u89e3\u5230\u8bc1\u660e\u6574\u5408\u7684\u5168\u8fc7\u7a0b\u3002\u901a\u8fc7\u8fd9\u4e9b\u4e13\u7528\u6218\u672f&#xff0c;DSL\u6709\u6548\u89e3\u51b3\u4e86Lean 4\u539f\u751f\u8bed\u6cd5\u5728\u9ad8\u7ea7\u8bc1\u660e\u8349\u56fe\u8bbe\u8ba1\u3001\u5b50\u95ee\u9898\u4e0a\u4e0b\u6587\u9694\u79bb\u548c\u8bc1\u660e\u81ea\u52a8\u6574\u5408\u65b9\u9762\u7684\u4e0d\u8db3&#xff0c;\u4e3a\u53cd\u5c04\u5f0f\u5206\u89e3\u63d0\u4f9b\u4e86\u575a\u5b9e\u7684\u6280\u672f\u57fa\u7840\u3002<\/p>\n<h4>\u6574\u4f53\u5de5\u4f5c\u6d41\u7a0b<\/h4>\n<p><img decoding=\"async\" src=\"https:\/\/www.wsisp.com\/helps\/wp-content\/uploads\/2025\/08\/20250810111446-68987f26a47b8.png\" alt=\"\u5728\u8fd9\u91cc\u63d2\u5165\u56fe\u7247\u63cf\u8ff0\" \/><\/p>\n<p>\u7b97\u6cd53\u63cf\u8ff0\u4e86Delta Prover\u7684\u5b8c\u6574\u5de5\u4f5c\u6d41\u7a0b&#xff0c;\u6574\u5408\u4e86\u4e0a\u8ff0\u6240\u6709\u7ec4\u4ef6&#xff1a;<\/p>\n<li>\u7cfb\u7edf\u9996\u5148\u5c1d\u8bd5\u901a\u8fc7\u8fed\u4ee3\u5f0f\u8bc1\u660e\u4fee\u590d\u76f4\u63a5\u89e3\u51b3\u539f\u5b9a\u7406\u3002<\/li>\n<li>\u82e5\u76f4\u63a5\u8bc1\u660e\u5931\u8d25&#xff0c;\u5219\u542f\u52a8\u53cd\u5c04\u5f0f\u5206\u89e3\u8fc7\u7a0b&#xff0c;\u751f\u6210\u5b50\u95ee\u9898\u5e76\u9010\u4e00\u6c42\u89e3\u3002<\/li>\n<li>\u5f53\u6240\u6709\u5b50\u95ee\u9898\u90fd\u5f97\u5230\u89e3\u51b3\u540e&#xff0c;\u7cfb\u7edf\u8fdb\u5165\u81ea\u52a8\u8bc1\u660e\u6574\u5408\u9636\u6bb5&#xff0c;\u901a\u8fc7DSL\u5c06\u5b50\u8bc1\u660e\u7ec4\u88c5\u4e3a\u539f\u5b9a\u7406\u7684\u5b8c\u6574\u8bc1\u660e\u3002<\/li>\n<li>\u82e5\u4efb\u4f55\u9636\u6bb5\u5931\u8d25\u4e14\u8fbe\u5230\u6700\u5927\u5c1d\u8bd5\u6b21\u6570&#xff0c;\u7cfb\u7edf\u6700\u7ec8\u8fd4\u56de\u5931\u8d25\u3002<\/li>\n<p>\u8fd9\u79cd\u5206\u5c42\u7b56\u7565\u786e\u4fdd\u4e86\u7cfb\u7edf\u7684\u6548\u7387\u548c\u9c81\u68d2\u6027&#xff1a;\u7b80\u5355\u95ee\u9898\u53ef\u4ee5\u901a\u8fc7\u76f4\u63a5\u8bc1\u660e\u5feb\u901f\u89e3\u51b3&#xff0c;\u800c\u590d\u6742\u95ee\u9898\u5219\u901a\u8fc7\u5206\u89e3\u964d\u4f4e\u96be\u5ea6\u3002\u6574\u4e2a\u8fc7\u7a0b\u65e0\u9700\u4efb\u4f55\u6a21\u578b\u5fae\u8c03&#xff0c;\u5b8c\u5168\u4f9d\u8d56\u901a\u7528\u5927\u6a21\u578b\u5728\u6846\u67b6\u5f15\u5bfc\u4e0b\u7684\u63a8\u7406\u80fd\u529b&#xff0c;\u663e\u8457\u964d\u4f4e\u4e86\u7cfb\u7edf\u6784\u5efa\u548c\u7ef4\u62a4\u7684\u6210\u672c\u3002<\/p>\n<h3>\u5b9e\u9a8c\u9a8c\u8bc1&#xff1a;\u5237\u65b0\u5f62\u5f0f\u5316\u8bc1\u660e\u6027\u80fd\u7eaa\u5f55<\/h3>\n<p>\u4e3a\u9a8c\u8bc1Delta Prover\u7684\u6709\u6548\u6027&#xff0c;\u5b57\u8282\u8df3\u52a8\u56e2\u961f\u8fdb\u884c\u4e86\u5168\u9762\u7684\u5b9e\u9a8c\u8bc4\u4f30&#xff0c;\u5728\u6807\u51c6\u57fa\u51c6\u6d4b\u8bd5\u4e0a\u4e0e\u73b0\u6709\u6700\u5148\u8fdb\u65b9\u6cd5\u8fdb\u884c\u4e86\u7cfb\u7edf\u6bd4\u8f83&#xff0c;\u5e76\u901a\u8fc7\u6d88\u878d\u5b9e\u9a8c\u91cf\u5316\u4e86\u5404\u6838\u5fc3\u7ec4\u4ef6\u7684\u8d21\u732e\u3002\u5b9e\u9a8c\u7ed3\u679c\u4e0d\u4ec5\u5c55\u793a\u4e86Delta Prover\u7684\u5353\u8d8a\u6027\u80fd&#xff0c;\u66f4\u63ed\u793a\u4e86\u901a\u7528\u5927\u6a21\u578b\u5728\u5f62\u5f0f\u5316\u63a8\u7406\u4e2d\u7684\u5de8\u5927\u6f5c\u529b\u3002<\/p>\n<h4>\u5b9e\u9a8c\u8bbe\u7f6e<\/h4>\n<p>\u5b9e\u9a8c\u91c7\u7528Gemini 2.5 Pro 05-06\u4f5c\u4e3a\u57fa\u7840\u5927\u6a21\u578b&#xff0c;\u8fd9\u662f\u4e00\u79cd\u672a\u7ecf\u8fc7\u5f62\u5f0f\u5316\u8bc1\u660e\u4e13\u95e8\u8bad\u7ec3\u7684\u901a\u7528\u5927\u6a21\u578b\u3002\u9009\u62e9\u8be5\u6a21\u578b\u65e8\u5728\u9a8c\u8bc1\u901a\u7528\u5927\u6a21\u578b\u5728\u6709\u6548\u6846\u67b6\u5f15\u5bfc\u4e0b\u7684\u5f62\u5f0f\u5316\u8bc1\u660e\u80fd\u529b&#xff0c;\u800c\u975e\u4f9d\u8d56\u6a21\u578b\u7684\u4e13\u95e8\u5316\u8bad\u7ec3\u3002\u91c7\u6837\u53c2\u6570\u8bbe\u7f6e\u4e3atemperature&#061;1&#xff0c;\u7b26\u5408\u901a\u7528\u5927\u6a21\u578b\u7684\u5178\u578b\u4f7f\u7528\u573a\u666f\u3002<\/p>\n<p>\u8bc4\u4f30\u4e3b\u8981\u57fa\u4e8e\u4e24\u4e2a\u6807\u51c6\u57fa\u51c6&#xff1a;<\/p>\n<ul>\n<li>miniF2F-test&#xff1a;\u8fd9\u662fminiF2F\u57fa\u51c6\u7684\u6d4b\u8bd5\u96c6&#xff0c;\u5305\u542b244\u4e2a\u6765\u81ea\u6570\u5b66\u7ade\u8d5b\u548cMATH\u6570\u636e\u96c6\u7684\u95ee\u9898&#xff0c;\u6db5\u76d6\u4e0d\u540c\u96be\u5ea6\u7ea7\u522b\u3002\u5b9e\u9a8c\u4f7f\u7528\u5176Lean 4\u7248\u672c&#xff0c;\u5e76\u4fee\u6b63\u4e86\u9648\u8ff0\u4e2d\u7684\u9519\u8bef\u4ee5\u786e\u4fdd\u516c\u5e73\u6bd4\u8f83\u3002<\/li>\n<li>miniF2F-test-IMO&#xff1a;\u4eceminiF2F-test\u4e2d\u63d0\u53d6\u7684\u56fd\u9645\u6570\u5b66\u5965\u6797\u5339\u514b&#xff08;IMO&#xff09;\u95ee\u9898\u5b50\u96c6&#xff0c;\u4ee3\u8868\u66f4\u5177\u6311\u6218\u6027\u7684\u5f62\u5f0f\u5316\u8bc1\u660e\u4efb\u52a1\u3002<\/li>\n<\/ul>\n<p>\u8fd9\u4e9b\u57fa\u51c6\u88ab\u5e7f\u6cdb\u7528\u4e8e\u8bc4\u4f30\u81ea\u52a8\u5b9a\u7406\u8bc1\u660e\u7cfb\u7edf\u7684\u6027\u80fd&#xff0c;\u63d0\u4f9b\u4e86\u4e0e\u73b0\u6709\u65b9\u6cd5\u7684\u76f4\u63a5\u6bd4\u8f83\u57fa\u7840\u3002<\/p>\n<h4>\u57fa\u51c6\u6027\u80fd\u6bd4\u8f83<\/h4>\n<p><img decoding=\"async\" src=\"https:\/\/www.wsisp.com\/helps\/wp-content\/uploads\/2025\/08\/20250810111447-68987f27ad699.png\" alt=\"\u5728\u8fd9\u91cc\u63d2\u5165\u56fe\u7247\u63cf\u8ff0\" \/><br \/>\n\u88681\u5c55\u793a\u4e86Delta Prover\u4e0e\u73b0\u6709\u6700\u5148\u8fdb\u65b9\u6cd5\u5728miniF2F-test\u4e0a\u7684\u6027\u80fd\u6bd4\u8f83\u3002\u7ed3\u679c\u663e\u793a&#xff0c;Delta Prover\u4ee595.9%\u7684\u6210\u529f\u7387\u521b\u4e0b\u65b0\u7684\u6027\u80fd\u7eaa\u5f55&#xff0c;\u663e\u8457\u8d85\u8d8a\u4e86\u6240\u6709\u73b0\u6709\u65b9\u6cd5&#xff0c;\u5305\u62ec\u9700\u8981\u5927\u91cf\u4e13\u95e8\u8bad\u7ec3\u7684\u6a21\u578b\u3002<\/p>\n<p>\u503c\u5f97\u6ce8\u610f\u7684\u662f&#xff0c;Delta Prover\u662f\u552f\u4e00\u65e0\u9700\u989d\u5916\u8bad\u7ec3\u7684\u65b9\u6cd5\u3002\u76f8\u6bd4\u4e4b\u4e0b&#xff0c;\u6b64\u524d\u7684\u6700\u4f73\u65b9\u6cd5Kimina Prover 72B\u867d\u7136\u8fbe\u523092.2%\u7684\u6210\u529f\u7387&#xff0c;\u4f46\u9700\u8981\u4e13\u95e8\u7684\u5fae\u8c03\u8bad\u7ec3\u548c\u9ad8\u8fbe42000\u7684\u6837\u672c\u9884\u7b97&#xff1b;DeepSeek-Prover-V2 671B\u7684\u6210\u529f\u7387\u4e3a88.9%&#xff0c;\u540c\u6837\u4f9d\u8d56\u4e8e\u4e13\u95e8\u8bad\u7ec3\u3002\u66f4\u4ee4\u4eba\u5370\u8c61\u6df1\u523b\u7684\u662f&#xff0c;\u5f53\u4f7f\u7528\u76f8\u540c\u7684Gemini 2.5 Pro\u6a21\u578b\u4f46\u91c7\u7528\u6807\u51c6\u7684Best-of-N\u7b56\u7565\u65f6&#xff0c;\u6210\u529f\u7387\u4ec5\u4e3a49.1%&#xff0c;\u8fd9\u5145\u5206\u8bc1\u660e\u4e86Delta Prover\u6846\u67b6\u5bf9\u91ca\u653e\u5927\u6a21\u578b\u80fd\u529b\u7684\u5173\u952e\u4f5c\u7528\u3002<\/p>\n<p>\u5728\u66f4\u5177\u6311\u6218\u6027\u7684miniF2F-test-IMO\u57fa\u51c6\u4e0a&#xff0c;Delta Prover\u540c\u6837\u8868\u73b0\u51fa\u8272&#xff0c;\u8fbe\u523085%\u7684\u6210\u529f\u7387&#xff0c;\u8d85\u8fc7\u4e86\u6b64\u524dDeepSeek-Prover-V2\u7b49\u65b9\u6cd5\u7684\u6027\u80fd&#xff0c;\u5c55\u793a\u4e86\u5176\u5904\u7406\u9ad8\u96be\u5ea6\u6570\u5b66\u95ee\u9898\u7684\u80fd\u529b\u3002\u8fd9\u4e00\u7ed3\u679c\u5c24\u4e3a\u91cd\u8981&#xff0c;\u56e0\u4e3aIMO\u95ee\u9898\u5386\u6765\u88ab\u89c6\u4e3a\u81ea\u52a8\u5b9a\u7406\u8bc1\u660e\u7684\u91cd\u5927\u6311\u6218&#xff0c;\u9700\u8981\u6df1\u523b\u7684\u6570\u5b66\u6d1e\u5bdf\u529b\u548c\u590d\u6742\u7684\u63a8\u7406\u94fe\u3002<\/p>\n<h4>\u6d4b\u8bd5\u65f6\u7f29\u653e\u7279\u6027<\/h4>\n<p><img decoding=\"async\" src=\"https:\/\/www.wsisp.com\/helps\/wp-content\/uploads\/2025\/08\/20250810111449-68987f29d59ca.png\" alt=\"\u5728\u8fd9\u91cc\u63d2\u5165\u56fe\u7247\u63cf\u8ff0\" \/><\/p>\n<p>\u9664\u4e86\u7edd\u5bf9\u6027\u80fd\u5916&#xff0c;\u6d4b\u8bd5\u65f6\u7684\u7f29\u653e\u7279\u6027&#xff08;scaling law&#xff09;\u662f\u8bc4\u4f30\u8bc1\u660e\u7cfb\u7edf\u5b9e\u7528\u6027\u7684\u53e6\u4e00\u5173\u952e\u6307\u6807&#xff0c;\u5b83\u53cd\u6620\u4e86\u7cfb\u7edf\u968f\u8ba1\u7b97\u8d44\u6e90\u589e\u52a0\u800c\u63d0\u5347\u6027\u80fd\u7684\u80fd\u529b\u3002\u56fe4\u5c55\u793a\u4e86Delta Prover\u5728\u4e24\u4e2a\u57fa\u51c6\u4e0a\u7684\u6d4b\u8bd5\u65f6\u7f29\u653e\u66f2\u7ebf&#xff0c;\u7ed3\u679c\u8868\u660e\u5176\u7f29\u653e\u7279\u6027\u663e\u8457\u4f18\u4e8e\u4f20\u7edf\u7684Best-of-N\u7b56\u7565\u3002<\/p>\n<p>\u8fd9\u79cd\u4f18\u52bf\u6e90\u4e8eDelta Prover\u7684\u8fed\u4ee3\u4f18\u5316\u673a\u5236&#xff1a;\u7cfb\u7edf\u80fd\u591f\u57fa\u4e8e\u5148\u524d\u5c1d\u8bd5\u7684\u53cd\u9988\u4e0d\u65ad\u6539\u8fdb\u8bc1\u660e&#xff0c;\u800c\u4e0d\u662f\u751f\u6210\u72ec\u7acb\u7684\u8bc1\u660e\u5c1d\u8bd5\u3002\u968f\u7740\u8ba1\u7b97\u9884\u7b97\u7684\u589e\u52a0&#xff0c;\u8fd9\u79cd\u7d2f\u79ef\u6539\u8fdb\u6548\u5e94\u4f7f\u5f97\u6027\u80fd\u63d0\u5347\u66f4\u52a0\u663e\u8457\u3002\u76f8\u6bd4\u4e4b\u4e0b&#xff0c;Best-of-N\u7b56\u7565\u7684\u6027\u80fd\u5f88\u5feb\u8d8b\u4e8e\u9971\u548c&#xff0c;\u56e0\u4e3a\u72ec\u7acb\u6837\u672c\u4e4b\u95f4\u65e0\u6cd5\u5171\u4eab\u4fe1\u606f\u6216\u76f8\u4e92\u5b66\u4e60\u3002<\/p>\n<p>Delta Prover\u7684\u6837\u672c\u9884\u7b97\u8ba1\u7b97\u65b9\u5f0f\u4e5f\u503c\u5f97\u6ce8\u610f&#xff1a;\u7cfb\u7edf\u8bb0\u5f55\u6bcf\u4e2a\u95ee\u9898\u6210\u529f\u89e3\u51b3\u6240\u9700\u7684API\u8c03\u7528\u6b21\u6570&#xff0c;\u6700\u7ec8\u9884\u7b97\u53d6\u6240\u6709\u5df2\u89e3\u51b3\u95ee\u9898\u4e2d\u7684\u6700\u5927\u503c\u3002\u8fd9\u79cd\u65b9\u5f0f\u786e\u4fdd\u4e86\u9884\u7b97\u4f30\u8ba1\u7684\u4fdd\u5b88\u6027&#xff0c;\u66f4\u771f\u5b9e\u5730\u53cd\u6620\u4e86\u5b9e\u9645\u4f7f\u7528\u573a\u666f\u4e2d\u7684\u8d44\u6e90\u9700\u6c42\u3002<\/p>\n<h4>\u6d88\u878d\u5b9e\u9a8c&#xff1a;\u6838\u5fc3\u7ec4\u4ef6\u7684\u8d21\u732e\u5206\u6790<\/h4>\n<p>\u4e3a\u91cf\u5316\u5404\u6838\u5fc3\u7ec4\u4ef6\u7684\u8d21\u732e&#xff0c;\u7814\u7a76\u56e2\u961f\u8fdb\u884c\u4e86\u7cfb\u7edf\u7684\u6d88\u878d\u5b9e\u9a8c&#xff0c;\u5206\u522b\u8bc4\u4f30\u4e86\u8fed\u4ee3\u5f0f\u8bc1\u660e\u4fee\u590d\u548c\u53cd\u5c04\u5f0f\u5206\u89e3\u7684\u5355\u72ec\u5f71\u54cd\u3002<\/p>\n<p>\u8fed\u4ee3\u5f0f\u8bc1\u660e\u4fee\u590d\u7684\u5f71\u54cd\u5b9e\u9a8c\u901a\u8fc7\u4e24\u79cd\u8bbe\u7f6e\u6bd4\u8f83&#xff1a;\u56fa\u5b9a\u603b\u9884\u7b97\u4e3a1024&#xff0c;\u6539\u53d8\u6bcf\u8f6e\u4fee\u590d\u6b21\u6570&#xff08;n&#xff09;\u548c\u8f6e\u6570&#xff08;m&#xff09;&#xff1b;\u4ee5\u53ca\u6bd4\u8f83\u7eaf\u4fee\u590d\u7b56\u7565&#xff08;m&#061;1&#xff09;\u4e0e\u7eaf\u91c7\u6837\u7b56\u7565&#xff08;n&#061;1&#xff09;\u7684\u6027\u80fd\u5dee\u5f02\u3002<br \/>\n<img decoding=\"async\" src=\"https:\/\/www.wsisp.com\/helps\/wp-content\/uploads\/2025\/08\/20250810111453-68987f2d646d0.png\" alt=\"\u5728\u8fd9\u91cc\u63d2\u5165\u56fe\u7247\u63cf\u8ff0\" \/><\/p>\n<p>\u5de6\u56fe\u7ed3\u679c\u663e\u793a&#xff0c;\u5728\u56fa\u5b9a\u603b\u9884\u7b97\u4e0b&#xff0c;\u589e\u52a0\u4fee\u590d\u6b21\u6570&#xff08;n&#xff09;\u6bd4\u589e\u52a0\u72ec\u7acb\u8f6e\u6570&#xff08;m&#xff09;\u80fd\u5e26\u6765\u66f4\u9ad8\u7684\u6210\u529f\u7387\u3002\u8fd9\u4e00\u53d1\u73b0\u4e0e\u4f20\u7edf\u7684\u63a2\u7d22-\u5229\u7528\u6743\u8861\u76f4\u89c9\u76f8\u53cd&#xff0c;\u8868\u660e\u5f53\u4ee3\u5927\u6a21\u578b\u5177\u6709\u5f3a\u5927\u7684\u81ea\u6211\u4fee\u6b63\u80fd\u529b&#xff0c;\u901a\u8fc7\u6df1\u5165\u4f18\u5316\u5355\u4e2a\u8bc1\u660e\u8f68\u8ff9\u6bd4\u63a2\u7d22\u591a\u4e2a\u72ec\u7acb\u8f68\u8ff9\u66f4\u6709\u6548\u3002<\/p>\n<p>\u53f3\u56fe\u6bd4\u8f83\u4e86\u8fed\u4ee3\u4fee\u590d&#xff08;m&#061;1&#xff09;\u4e0eBest-of-N\u91c7\u6837&#xff08;n&#061;1&#xff09;\u7684\u6027\u80fd&#xff0c;\u7ed3\u679c\u6e05\u6670\u5730\u8868\u660e\u8fed\u4ee3\u4fee\u590d\u7b56\u7565\u5728\u6240\u6709\u9884\u7b97\u6c34\u5e73\u4e0a\u90fd\u4f18\u4e8e\u91c7\u6837\u7b56\u7565&#xff0c;\u4e14\u4f18\u52bf\u968f\u9884\u7b97\u589e\u52a0\u800c\u6269\u5927\u3002\u8fd9\u9a8c\u8bc1\u4e86\u8fed\u4ee3\u53cd\u9988\u5faa\u73af\u5728\u91ca\u653e\u5927\u6a21\u578b\u63a8\u7406\u80fd\u529b\u4e2d\u7684\u5173\u952e\u4f5c\u7528\u3002<\/p>\n<p>\u53cd\u5c04\u5f0f\u5206\u89e3\u7684\u5f71\u54cd\u5b9e\u9a8c\u9009\u53d6\u4e86IMO 2019 Problem 1\u4f5c\u4e3a\u6d4b\u8bd5\u6848\u4f8b&#xff0c;\u8fd9\u4e00\u95ee\u9898\u5bf9\u73b0\u6709\u81ea\u52a8\u8bc1\u660e\u5668\u6781\u5177\u6311\u6218\u6027&#xff0c;\u5305\u62ecDeepSeek-Prover-V2\u5728\u5185\u7684\u65b9\u6cd5\u5747\u672a\u80fd\u89e3\u51b3\u3002<\/p>\n<p>\u5b9e\u9a8c\u5bf9\u6bd4\u4e86\u4e24\u79cd\u7b56\u7565&#xff1a;\u4ec5\u4f7f\u7528\u8fed\u4ee3\u5f0f\u8bc1\u660e\u4fee\u590d\u7684\u57fa\u7ebf\u65b9\u6cd5&#xff0c;\u4ee5\u53ca\u5b8c\u6574\u7684Delta Prover&#xff08;\u5305\u542b\u53cd\u5c04\u5f0f\u5206\u89e3&#xff09;\u3002\u7ed3\u679c\u663e\u793a&#xff0c;\u57fa\u7ebf\u65b9\u6cd5\u57281024\u6b21API\u8c03\u7528\u540e\u4ecd\u672a\u80fd\u627e\u5230\u89e3\u51b3\u65b9\u6848&#xff1b;\u800cDelta Prover\u901a\u8fc7\u5c06\u95ee\u9898\u5206\u89e3\u4e3a83\u4e2a\u5b50\u95ee\u9898&#xff0c;\u5e73\u5747\u6bcf\u4e2a\u5b50\u95ee\u9898\u4ec5\u97004\u6b21API\u8c03\u7528&#xff0c;\u603b\u5171\u7ea6332\u6b21\u8c03\u7528\u5373\u6210\u529f\u89e3\u51b3\u4e86\u95ee\u9898\u3002\u8fd9\u4e00\u7ed3\u679c\u4e0d\u4ec5\u8bc1\u660e\u4e86\u53cd\u5c04\u5f0f\u5206\u89e3\u5bf9\u5904\u7406\u590d\u6742\u95ee\u9898\u7684\u6709\u6548\u6027&#xff0c;\u4e5f\u5c55\u793a\u4e86\u5176\u663e\u8457\u7684\u6548\u7387\u4f18\u52bf\u3002<\/p>\n<p>\u5206\u89e3\u540e\u7684\u5b50\u95ee\u9898\u8986\u76d6\u4e86\u4ece\u57fa\u7840\u5f15\u7406\u5230\u5173\u952e\u6b65\u9aa4\u7684\u5404\u4e2a\u65b9\u9762&#xff0c;\u5f62\u6210\u4e86\u5c42\u6b21\u5316\u7684\u8bc1\u660e\u7ed3\u6784\u3002\u4f8b\u5982&#xff0c;\u7cfb\u7edf\u9996\u5148\u5efa\u7acb\u4e86\u51fd\u6570\u7684\u57fa\u672c\u6027\u8d28&#xff08;\u5982f(2a)\u7684\u8868\u8fbe\u5f0f&#xff09;&#xff0c;\u7136\u540e\u63a8\u5bfc\u51fa\u9012\u5f52\u5173\u7cfb&#xff0c;\u6700\u7ec8\u901a\u8fc7\u5206\u7c7b\u8ba8\u8bba\u786e\u5b9a\u51fd\u6570\u5f62\u5f0f\u3002\u8fd9\u79cd\u7ed3\u6784\u5316\u5206\u89e3\u5b8c\u7f8e\u4f53\u73b0\u4e86\u4eba\u7c7b\u6570\u5b66\u5bb6\u89e3\u51b3\u590d\u6742\u95ee\u9898\u7684\u7b56\u7565&#xff0c;\u5c55\u793a\u4e86\u5927\u6a21\u578b\u5728\u6846\u67b6\u5f15\u5bfc\u4e0b\u6a21\u62df\u9ad8\u7ea7\u6570\u5b66\u63a8\u7406\u7684\u80fd\u529b\u3002<\/p>\n<h4>\u5178\u578b\u6848\u4f8b\u5206\u6790<\/h4>\n<p>\u4e3a\u8fdb\u4e00\u6b65\u7406\u89e3Delta Prover\u7684\u5de5\u4f5c\u673a\u5236&#xff0c;\u7814\u7a76\u56e2\u961f\u5206\u6790\u4e86\u591a\u4e2a\u5178\u578b\u6848\u4f8b&#xff0c;\u63ed\u793a\u4e86\u7cfb\u7edf\u5728\u9762\u5bf9\u4e0d\u540c\u7c7b\u578b\u6311\u6218\u65f6\u7684\u5e94\u5bf9\u7b56\u7565\u3002<\/p>\n<p>\u68c0\u7d22\u589e\u5f3a\u4fee\u590d\u6848\u4f8b\u5c55\u793a\u4e86\u7cfb\u7edf\u5982\u4f55\u5904\u7406\u5b9a\u7406\u540d\u79f0\u9519\u8bef\u3002\u5728\u4e00\u4e2a\u6c42\u548c\u95ee\u9898\u4e2d&#xff0c;\u5927\u6a21\u578b\u6700\u521d\u4f7f\u7528\u4e86\u9519\u8bef\u7684\u5b9a\u7406\u540d\u79f0AntitoneOn.sum_le_integral_Icc&#xff0c;\u7cfb\u7edf\u7684\u68c0\u7d22\u673a\u5236\u57fa\u4e8e\u8fd9\u4e00\u9519\u8bef\u540d\u79f0\u627e\u5230\u4e86\u6b63\u786e\u7684\u5b9a\u7406AntitoneOn.sum_le_integral_Ico\u53ca\u5176\u7b7e\u540d&#xff0c;\u5e76\u5c06\u5176\u4f5c\u4e3a\u63d0\u793a\u63d0\u4f9b\u7ed9\u5927\u6a21\u578b&#xff0c;\u6700\u7ec8\u6210\u529f\u5b8c\u6210\u8bc1\u660e\u3002\u8fd9\u4e00\u8fc7\u7a0b\u5c55\u793a\u4e86\u68c0\u7d22\u589e\u5f3a\u5728\u5f25\u8865\u5927\u6a21\u578b\u77e5\u8bc6\u7f3a\u53e3\u65b9\u9762\u7684\u5173\u952e\u4f5c\u7528\u3002<\/p>\n<p>\u591a\u6b65\u8fed\u4ee3\u4fee\u590d\u6848\u4f8b\u5c55\u793a\u4e86\u7cfb\u7edf\u7684\u590d\u6742\u9519\u8bef\u4fee\u6b63\u80fd\u529b\u3002\u5728\u4e00\u4e2a\u4ee3\u6570\u95ee\u9898\u4e2d&#xff0c;\u5927\u6a21\u578b\u9996\u5148\u5c1d\u8bd5\u4f7f\u7528mul_div_cancel_left\u5b9a\u7406\u5931\u8d25&#xff1b;\u53cd\u601d\u540e\u8f6c\u800c\u4f7f\u7528simp\u6218\u672f&#xff0c;\u4f46Lean\u53cd\u9988simp\u65e0\u6cd5\u5b8c\u6210\u6570\u503c\u7b80\u5316&#xff1b;\u5927\u6a21\u578b\u518d\u6b21\u8c03\u6574\u7b56\u7565&#xff0c;\u660e\u786e\u8c03\u7528norm_num\u5b8c\u6210\u6570\u503c\u7b80\u5316&#xff0c;\u6700\u7ec8\u6210\u529f\u3002\u8fd9\u4e00\u8fc7\u7a0b\u5c55\u793a\u4e86\u7cfb\u7edf\u901a\u8fc7\u591a\u8f6e\u53cd\u601d\u9010\u6b65\u903c\u8fd1\u6b63\u786e\u89e3\u7684\u80fd\u529b\u3002<\/p>\n<p>\u590d\u6742\u95ee\u9898\u5206\u89e3\u6848\u4f8b\u8be6\u7ec6\u5206\u6790\u4e86IMO 2019 P1\u7684\u5206\u89e3\u8fc7\u7a0b\u3002\u7cfb\u7edf\u5c06\u8fd9\u4e00\u6311\u6218\u6027\u95ee\u9898\u5206\u89e3\u4e3a83\u4e2a\u5b50\u95ee\u9898&#xff0c;\u6db5\u76d6\u4ece\u57fa\u672c\u66ff\u6362\u5230\u6700\u7ec8\u7ed3\u8bba\u7684\u5404\u4e2a\u6b65\u9aa4\u3002\u4f8b\u5982&#xff0c;\u901a\u8fc7\u8bbe\u7f6e\u7279\u5b9a\u53d8\u91cf\u503c&#xff08;a&#061;0\u6216b&#061;0&#xff09;\u63a8\u5bfc\u5173\u952e\u65b9\u7a0b&#xff0c;\u5efa\u7acb\u9012\u5f52\u5173\u7cfb&#xff0c;\u6c42\u89e3\u9012\u5f52\u5f97\u5230\u51fd\u6570\u5f62\u5f0f&#xff0c;\u6700\u540e\u901a\u8fc7\u5206\u7c7b\u8ba8\u8bba\u5b8c\u6210\u8bc1\u660e\u3002\u8fd9\u79cd\u7cbe\u7ec6\u5206\u89e3\u4f7f\u539f\u672c\u96be\u4ee5\u76f4\u63a5\u8bc1\u660e\u7684\u590d\u6742\u95ee\u9898\u53d8\u5f97\u53ef\u89e3&#xff0c;\u5145\u5206\u5c55\u793a\u4e86\u53cd\u5c04\u5f0f\u5206\u89e3\u7684\u5a01\u529b\u3002<\/p>\n<p>\u8fd9\u4e9b\u6848\u4f8b\u5171\u540c\u8bc1\u660e\u4e86Delta Prover\u6846\u67b6\u7684\u9c81\u68d2\u6027\u548c\u9002\u5e94\u6027&#xff0c;\u80fd\u591f\u5904\u7406\u5f62\u5f0f\u5316\u8bc1\u660e\u4e2d\u5e38\u89c1\u7684\u5404\u79cd\u6311\u6218&#xff0c;\u4ece\u7b80\u5355\u7684\u8bed\u6cd5\u9519\u8bef\u5230\u590d\u6742\u7684\u7b56\u7565\u8c03\u6574\u3002<\/p>\n<p>\u610f\u4e49\u4e0e\u5c55\u671b&#xff1a;\u91cd\u65b0\u5b9a\u4e49 AI \u5f62\u5f0f\u5316\u63a8\u7406\u7684\u672a\u6765<\/p>\n<p>Delta Prover \u7684\u7a81\u7834\u6027\u6210\u679c\u4e0d\u4ec5\u5237\u65b0\u4e86\u81ea\u52a8\u5b9a\u7406\u8bc1\u660e\u7684\u6027\u80fd\u7eaa\u5f55&#xff0c;\u66f4\u5728\u65b9\u6cd5\u8bba\u4e0a\u4e3a AI \u5f62\u5f0f\u5316\u63a8\u7406\u5f00\u8f9f\u4e86\u65b0\u8def\u5f84&#xff0c;\u5176\u610f\u4e49\u4e0e\u5f71\u54cd\u503c\u5f97\u6df1\u5165\u63a2\u8ba8\u3002<br \/>\n\u5bf9 AI \u63a8\u7406\u7814\u7a76\u7684\u542f\u793a<\/p>\n<p>Delta Prover \u6700\u6df1\u8fdc\u7684\u8d21\u732e\u5728\u4e8e\u8bc1\u660e\u4e86\u901a\u7528\u5927\u6a21\u578b\u5728\u9002\u5f53\u6846\u67b6\u5f15\u5bfc\u4e0b&#xff0c;\u65e0\u9700\u4e13\u95e8\u8bad\u7ec3\u5373\u53ef\u5728\u9ad8\u5ea6\u4e13\u4e1a\u5316\u7684\u5f62\u5f0f\u5316\u8bc1\u660e\u4efb\u52a1\u4e2d\u8fbe\u5230\u751a\u81f3\u8d85\u8d8a\u4e13\u95e8\u6a21\u578b\u7684\u6c34\u5e73\u3002\u8fd9\u4e00\u53d1\u73b0\u6311\u6218\u4e86 \u201c\u9886\u57df\u4e13\u7cbe\u5fc5\u987b\u4f9d\u8d56\u9886\u57df\u5fae\u8c03\u201d \u7684\u4f20\u7edf\u8ba4\u77e5&#xff0c;\u8868\u660e\u901a\u7528\u5927\u6a21\u578b\u7684\u63a8\u7406\u548c\u53cd\u601d\u80fd\u529b\u5df2\u7ecf\u53d1\u5c55\u5230\u53ef\u4ee5\u901a\u8fc7\u6709\u6548\u5f15\u5bfc\u6765\u638c\u63e1\u9ad8\u5ea6\u4e13\u4e1a\u5316\u6280\u80fd\u7684\u9636\u6bb5\u3002<\/p>\n<p>\u7814\u7a76\u7ed3\u679c\u51f8\u663e\u4e86 \u201c\u6846\u67b6\u8bbe\u8ba1\u201d \u800c\u975e \u201c\u6a21\u578b\u8bad\u7ec3\u201d \u5728\u91ca\u653e AI \u80fd\u529b\u4e2d\u7684\u5173\u952e\u4f5c\u7528\u3002Delta Prover \u901a\u8fc7\u6784\u5efa\u53cd\u5c04\u5f0f\u5206\u89e3\u4e0e\u8fed\u4ee3\u4fee\u590d\u7684\u534f\u540c\u673a\u5236&#xff0c;\u521b\u9020\u4e86\u4e00\u79cd \u201c\u601d\u8003 &#8211; \u5c1d\u8bd5 &#8211; \u4fee\u6b63 &#8211; \u518d\u601d\u8003\u201d \u7684\u95ed\u73af\u63a8\u7406\u8fc7\u7a0b&#xff0c;\u8fd9\u4e0e\u4eba\u8111\u89e3\u51b3\u590d\u6742\u95ee\u9898\u7684\u8ba4\u77e5\u6a21\u5f0f\u9ad8\u5ea6\u76f8\u4f3c\u3002\u8fd9\u79cd agentic \u67b6\u6784\u4e3a\u8bbe\u8ba1\u4e0b\u4e00\u4ee3 AI \u63a8\u7406\u7cfb\u7edf\u63d0\u4f9b\u4e86\u91cd\u8981\u53c2\u8003&#xff1a;\u672a\u6765\u7684\u91cd\u70b9\u53ef\u80fd\u4e0d\u5728\u4e8e\u8bad\u7ec3\u66f4\u4e13\u4e1a\u7684\u6a21\u578b&#xff0c;\u800c\u5728\u4e8e\u6784\u5efa\u66f4\u667a\u80fd\u7684\u63a8\u7406\u6846\u67b6\u3002<\/p>\n<p>\u6b64\u5916&#xff0c;Delta Prover \u5c55\u793a\u4e86\u901a\u7528\u5927\u6a21\u578b\u5f3a\u5927\u7684\u5b50\u95ee\u9898\u5206\u89e3\u80fd\u529b\u3002\u5728 IMO 2019 Problem 1 \u7684\u6848\u4f8b\u4e2d&#xff0c;\u7cfb\u7edf\u80fd\u591f\u81ea\u4e3b\u5c06\u590d\u6742\u5b9a\u7406\u5206\u89e3\u4e3a 83 \u4e2a\u6709\u5e8f\u4f9d\u8d56\u7684\u5b50\u95ee\u9898&#xff0c;\u5f62\u6210\u5c42\u6b21\u5316\u7684\u8bc1\u660e\u7ed3\u6784\u3002\u8fd9\u79cd\u80fd\u529b\u8868\u660e\u5927\u6a21\u578b\u4e0d\u4ec5\u80fd\u8fdb\u884c\u6b65\u9aa4\u63a8\u7406&#xff0c;\u8fd8\u5177\u5907\u5168\u5c40\u89c4\u5212\u80fd\u529b&#xff0c;\u4e3a\u89e3\u51b3\u66f4\u5e7f\u6cdb\u7684\u590d\u6742\u95ee\u9898\u63d0\u4f9b\u4e86\u53ef\u80fd\u3002<br \/>\n\u5bf9\u6570\u5b66\u7814\u7a76\u4e0e\u6559\u80b2\u7684\u6f5c\u5728\u5f71\u54cd<\/p>\n<p>\u5f62\u5f0f\u5316\u6570\u5b66\u8bc1\u660e\u6280\u672f\u7684\u8fdb\u6b65\u5bf9\u6570\u5b66\u7814\u7a76\u548c\u6559\u80b2\u5177\u6709\u6df1\u8fdc\u610f\u4e49\u3002\u5bf9\u4e8e\u7814\u7a76\u800c\u8a00&#xff0c;Delta Prover \u7b49\u5148\u8fdb\u8bc1\u660e\u7cfb\u7edf\u6709\u671b\u6210\u4e3a\u6570\u5b66\u5bb6\u7684\u5f97\u529b\u52a9\u624b&#xff0c;\u627f\u62c5\u7e41\u7410\u7684\u7ec6\u8282\u9a8c\u8bc1\u5de5\u4f5c&#xff0c;\u8ba9\u7814\u7a76\u8005\u80fd\u591f\u4e13\u6ce8\u4e8e\u6838\u5fc3\u521b\u610f\u548c\u6218\u7565\u89c4\u5212\u3002\u7279\u522b\u662f\u5728\u590d\u6742\u5b9a\u7406\u7684\u8bc1\u660e\u4e2d&#xff0c;\u7cfb\u7edf\u53ef\u4ee5\u81ea\u52a8\u68c0\u67e5\u5f15\u7406\u7684\u6b63\u786e\u6027\u5e76\u63a2\u7d22\u53ef\u80fd\u7684\u8bc1\u660e\u8def\u5f84&#xff0c;\u52a0\u901f\u6570\u5b66\u53d1\u73b0\u8fc7\u7a0b\u3002<\/p>\n<p>\u5728\u6559\u80b2\u9886\u57df&#xff0c;\u9ad8\u6027\u80fd\u5f62\u5f0f\u5316\u8bc1\u660e\u7cfb\u7edf\u53ef\u4ee5\u4f5c\u4e3a\u4e2a\u6027\u5316\u5b66\u4e60\u5de5\u5177&#xff0c;\u4e3a\u5b66\u751f\u63d0\u4f9b\u5373\u65f6\u53cd\u9988\u548c\u8bc1\u660e\u6307\u5bfc\u3002\u901a\u8fc7\u5206\u6790\u5b66\u751f\u7684\u5f62\u5f0f\u5316\u8bc1\u660e\u5c1d\u8bd5&#xff0c;\u7cfb\u7edf\u53ef\u4ee5\u51c6\u786e\u8bc6\u522b\u7406\u89e3\u8bef\u533a\u5e76\u63d0\u4f9b\u9488\u5bf9\u6027\u5efa\u8bae&#xff0c;\u8fd9\u6bd4\u4f20\u7edf\u6559\u5b66\u65b9\u5f0f\u66f4\u9ad8\u6548\u3001\u66f4\u4e2a\u6027\u5316\u3002\u6b64\u5916&#xff0c;\u7cfb\u7edf\u751f\u6210\u7684\u8be6\u7ec6\u8bc1\u660e\u6b65\u9aa4\u4e5f\u53ef\u4f5c\u4e3a\u5b66\u4e60\u8d44\u6e90&#xff0c;\u5e2e\u52a9\u5b66\u751f\u7406\u89e3\u590d\u6742\u6570\u5b66\u6982\u5ff5\u7684\u63a8\u7406\u8fc7\u7a0b\u3002<\/p>\n<p>\u503c\u5f97\u6ce8\u610f\u7684\u662f&#xff0c;Delta Prover \u5728\u5904\u7406 IMO \u7ea7\u522b\u7684\u95ee\u9898\u4e0a\u53d6\u5f97\u7684\u7a81\u7834&#xff08;85% \u6210\u529f\u7387&#xff09;&#xff0c;\u8868\u660e AI \u7cfb\u7edf\u5df2\u7ecf\u5f00\u59cb\u63a5\u8fd1\u4eba\u7c7b\u6570\u5b66\u7ade\u8d5b\u9009\u624b\u7684\u6c34\u5e73\u3002\u8fd9\u4e0d\u4ec5\u4e3a\u6570\u5b66\u6559\u80b2\u63d0\u4f9b\u4e86\u65b0\u5de5\u5177&#xff0c;\u4e5f\u53ef\u80fd\u91cd\u65b0\u5b9a\u4e49\u4eba\u7c7b\u4e0e\u673a\u5668\u5728\u6570\u5b66\u521b\u9020\u529b\u65b9\u9762\u7684\u534f\u4f5c\u6a21\u5f0f\u3002<br \/>\n\u6280\u672f\u5c40\u9650\u6027\u4e0e\u672a\u6765\u65b9\u5411<\/p>\n<p>\u5c3d\u7ba1\u53d6\u5f97\u4e86\u663e\u8457\u6210\u529f&#xff0c;Delta Prover \u4ecd\u5b58\u5728\u6280\u672f\u5c40\u9650\u6027&#xff0c;\u8fd9\u4e9b\u6311\u6218\u4e5f\u6307\u660e\u4e86\u672a\u6765\u7684\u7814\u7a76\u65b9\u5411\u3002<\/p>\n<p>\u5f53\u524d\u7cfb\u7edf\u5728\u5904\u7406\u9700\u8981\u9ad8\u5ea6\u521b\u9020\u6027\u7684\u6570\u5b66\u6d1e\u5bdf\u65b9\u9762\u4ecd\u6709\u4e0d\u8db3\u3002\u867d\u7136\u53cd\u5c04\u5f0f\u5206\u89e3\u80fd\u591f\u5904\u7406\u5df2\u77e5\u7b56\u7565\u8303\u56f4\u5185\u7684\u95ee\u9898&#xff0c;\u4f46\u9762\u5bf9\u9700\u8981\u5168\u65b0\u8bc1\u660e\u601d\u8def\u7684\u95ee\u9898\u65f6&#xff0c;\u6027\u80fd\u53ef\u80fd\u5927\u5e45\u4e0b\u964d\u3002\u6b64\u5916&#xff0c;\u7cfb\u7edf\u5bf9\u5f62\u5f0f\u5316\u8bed\u8a00\u7684\u7406\u89e3\u4ecd\u4f9d\u8d56\u4e8e\u63d0\u793a\u5de5\u7a0b\u800c\u975e\u771f\u6b63\u7684\u8bed\u4e49\u7406\u89e3&#xff0c;\u8fd9\u53ef\u80fd\u5bfc\u81f4\u5728\u590d\u6742\u573a\u666f\u4e0b\u7684\u8bef\u89e3\u548c\u9519\u8bef\u3002<\/p>\n<p>\u9488\u5bf9\u8fd9\u4e9b\u5c40\u9650\u6027&#xff0c;\u7814\u7a76\u56e2\u961f\u63d0\u51fa\u4e86\u672a\u6765\u5de5\u4f5c\u7684\u51e0\u4e2a\u91cd\u8981\u65b9\u5411&#xff1a;<\/p>\n<p>\u63a2\u7d22\u66f4\u7cbe\u7ec6\u7684\u6d4b\u8bd5\u65f6\u6280\u672f&#xff1a;\u5982\u5f15\u5165\u8fdb\u5316\u7b97\u6cd5&#xff08;FunSearch\u3001AlphaEvolve \u7b49&#xff09;\u5b9e\u73b0\u52a8\u6001\u8bc1\u660e\u641c\u7d22\u4f18\u5316&#xff0c;\u8d85\u8d8a\u5f53\u524d\u9884\u5b9a\u4e49\u7684\u5de5\u4f5c\u6d41\u7a0b\u3002\u8fd9\u79cd\u65b9\u6cd5\u53ef\u4ee5\u8ba9\u7cfb\u7edf\u5728\u8bc1\u660e\u8fc7\u7a0b\u4e2d\u81ea\u4e3b\u53d1\u73b0\u65b0\u7684\u7b56\u7565\u548c\u6280\u5de7&#xff0c;\u63d0\u9ad8\u521b\u9020\u6027\u95ee\u9898\u89e3\u51b3\u80fd\u529b\u3002<br \/>\n\u57fa\u4e8e\u4ee3\u7406\u5de5\u4f5c\u6d41\u7684\u5f3a\u5316\u5b66\u4e60&#xff1a;\u901a\u8fc7\u5f3a\u5316\u5b66\u4e60\u8ba9\u4ee3\u7406\u4e0d\u65ad\u4f18\u5316\u8bc1\u660e\u7b56\u7565&#xff0c;\u4f7f\u5176\u80fd\u591f\u4ece\u5927\u91cf\u8bc1\u660e\u7ecf\u9a8c\u4e2d\u5b66\u4e60\u6709\u6548\u7684\u95ee\u9898\u5206\u89e3\u548c\u4fee\u590d\u6a21\u5f0f\u3002\u8fd9\u79cd\u65b9\u6cd5\u53ef\u4ee5\u8fdb\u4e00\u6b65\u63d0\u5347\u7cfb\u7edf\u7684\u81ea\u9002\u5e94\u80fd\u529b\u548c\u957f\u671f\u6027\u80fd\u3002<br \/>\n\u6269\u5c55 DSL \u80fd\u529b&#xff1a;\u589e\u5f3a\u9886\u57df\u7279\u5b9a\u8bed\u8a00\u5bf9\u66f4\u590d\u6742\u6570\u5b66\u7ed3\u6784\u7684\u652f\u6301&#xff0c;\u5982\u9ad8\u9636\u903b\u8f91\u3001\u8303\u7574\u8bba\u7b49&#xff0c;\u6269\u5927\u7cfb\u7edf\u7684\u5e94\u7528\u8303\u56f4\u3002\u540c\u65f6\u4f18\u5316\u5b50\u95ee\u9898\u7ba1\u7406\u673a\u5236&#xff0c;\u63d0\u9ad8\u5206\u89e3\u6548\u7387\u548c\u6574\u5408\u80fd\u529b\u3002<br \/>\n\u591a\u6a21\u6001\u8bc1\u660e\u8f85\u52a9&#xff1a;\u7ed3\u5408\u81ea\u7136\u8bed\u8a00\u7406\u89e3\u3001\u56fe\u8868\u8bc6\u522b\u548c\u5f62\u5f0f\u5316\u63a8\u7406&#xff0c;\u6784\u5efa\u66f4\u5168\u9762\u7684\u6570\u5b66\u95ee\u9898\u89e3\u51b3\u7cfb\u7edf\u3002\u8fd9\u5c06\u4f7f\u7cfb\u7edf\u80fd\u591f\u5904\u7406\u66f4\u5e7f\u6cdb\u7684\u8f93\u5165\u5f62\u5f0f&#xff0c;\u5305\u62ec\u6559\u79d1\u4e66\u95ee\u9898\u3001\u7814\u7a76\u8bba\u6587\u4e2d\u7684\u731c\u60f3\u7b49\u3002<br \/>\n\u66f4\u5e7f\u6cdb\u7684 AI \u4ee3\u7406\u7814\u7a76\u542f\u793a<\/p>\n<p>Delta Prover \u7684\u6210\u529f\u4e0d\u4ec5\u9650\u4e8e\u6570\u5b66\u8bc1\u660e\u9886\u57df&#xff0c;\u66f4\u4e3a\u901a\u7528 AI \u4ee3\u7406\u7814\u7a76\u63d0\u4f9b\u4e86\u91cd\u8981\u542f\u793a\u3002\u5176\u6838\u5fc3\u7ecf\u9a8c \u2014\u2014 \u901a\u8fc7\u6709\u6548\u7684\u6846\u67b6\u8bbe\u8ba1\u91ca\u653e\u901a\u7528\u5927\u6a21\u578b\u7684\u80fd\u529b \u2014\u2014 \u53ef\u4ee5\u63a8\u5e7f\u5230\u5176\u4ed6\u590d\u6742\u4efb\u52a1\u4e2d\u3002<\/p>\n<p>\u7cfb\u7edf\u5c55\u793a\u7684\u53cd\u5c04\u5f0f\u5206\u89e3\u548c\u8fed\u4ee3\u4fee\u590d\u673a\u5236\u4ee3\u8868\u4e86\u4e00\u79cd\u901a\u7528\u7684\u95ee\u9898\u89e3\u51b3\u8303\u5f0f&#xff1a;\u5c06\u590d\u6742\u4efb\u52a1\u5206\u89e3\u4e3a\u5b50\u4efb\u52a1&#xff0c;\u901a\u8fc7\u6301\u7eed\u53cd\u9988\u4f18\u5316\u5b50\u4efb\u52a1\u89e3\u51b3\u65b9\u6848&#xff0c;\u6700\u7ec8\u6574\u5408\u4e3a\u6574\u4f53\u7ed3\u679c\u3002\u8fd9\u79cd\u8303\u5f0f\u53ef\u5e94\u7528\u4e8e\u4ee3\u7801\u751f\u6210\u3001\u79d1\u5b66\u53d1\u73b0\u3001\u590d\u6742\u51b3\u7b56\u7b49\u591a\u4e2a\u9886\u57df&#xff0c;\u63a8\u52a8 AI \u7cfb\u7edf\u4ece\u5355\u4e00\u4efb\u52a1\u6267\u884c\u8005\u5411\u591a\u529f\u80fd\u95ee\u9898\u89e3\u51b3\u8005\u8f6c\u53d8\u3002<\/p>\n<p>\u6b64\u5916&#xff0c;Delta Prover \u65e0\u9700\u4e13\u95e8\u8bad\u7ec3\u7684\u7279\u6027\u5927\u5e45\u964d\u4f4e\u4e86\u6280\u672f\u5e94\u7528\u7684\u95e8\u69db\u3002\u4f01\u4e1a\u548c\u7814\u7a76\u673a\u6784\u65e0\u9700\u6295\u5165\u5de8\u989d\u8d44\u6e90\u8fdb\u884c\u6a21\u578b\u5fae\u8c03&#xff0c;\u53ea\u9700\u6784\u5efa\u9002\u5f53\u7684\u4ee3\u7406\u6846\u67b6\u5373\u53ef\u5c06\u901a\u7528\u5927\u6a21\u578b\u5e94\u7528\u4e8e\u7279\u5b9a\u9886\u57df&#xff0c;\u8fd9\u5c06\u52a0\u901f AI \u6280\u672f\u7684\u666e\u53ca\u548c\u521b\u65b0\u3002<\/p>\n<p>\u5728 AI \u4f26\u7406\u548c\u53ef\u89e3\u91ca\u6027\u65b9\u9762&#xff0c;Delta Prover \u7684\u900f\u660e\u5de5\u4f5c\u6d41\u7a0b\u4e5f\u5177\u6709\u4f18\u52bf\u3002\u7cfb\u7edf\u7684\u6bcf\u4e2a\u5206\u89e3\u6b65\u9aa4\u548c\u4fee\u590d\u51b3\u7b56\u90fd\u53ef\u4ee5\u88ab\u8ffd\u8e2a\u548c\u89e3\u91ca&#xff0c;\u8fd9\u6bd4\u9ed1\u7bb1\u5f0f\u7684\u5927\u578b\u6a21\u578b\u66f4\u6613\u4e8e\u7406\u89e3\u548c\u5ba1\u8ba1\u3002\u8fd9\u79cd\u53ef\u89e3\u91ca\u6027\u5bf9\u4e8e\u9ad8\u98ce\u9669\u9886\u57df\u7684 AI \u5e94\u7528\u81f3\u5173\u91cd\u8981\u3002<br \/>\n\u7ed3\u8bba&#xff1a;\u5f62\u5f0f\u5316\u63a8\u7406\u7684\u65b0\u65f6\u4ee3<\/p>\n<p>Delta Prover \u7684\u95ee\u4e16\u6807\u5fd7\u7740\u5f62\u5f0f\u5316\u6570\u5b66\u63a8\u7406\u8fdb\u5165\u4e86\u4e00\u4e2a\u65b0\u7684\u65f6\u4ee3\u3002\u901a\u8fc7\u521b\u65b0\u6027\u5730\u5c06\u901a\u7528\u5927\u6a21\u578b\u4e0e\u5f62\u5f0f\u5316\u8bc1\u660e\u73af\u5883\u76f8\u7ed3\u5408&#xff0c;\u5b57\u8282\u8df3\u52a8 Seed \u56e2\u961f\u4e0d\u4ec5\u5b9e\u73b0\u4e86\u6027\u80fd\u7a81\u7834&#xff0c;\u66f4\u5f00\u8f9f\u4e86\u4e00\u6761\u8d44\u6e90\u9ad8\u6548\u7684\u6280\u672f\u8def\u5f84\u3002\u7cfb\u7edf\u5728 miniF2F-test \u4e0a 95.9% \u7684\u6210\u529f\u7387\u548c\u5728 IMO \u95ee\u9898\u4e0a 85% \u7684\u6210\u529f\u7387&#xff0c;\u4e0d\u4ec5\u5237\u65b0\u4e86\u7eaa\u5f55&#xff0c;\u66f4\u8bc1\u660e\u4e86\u901a\u7528\u667a\u80fd\u4e0e\u5f62\u5f0f\u5316\u63a8\u7406\u7ed3\u5408\u7684\u5de8\u5927\u6f5c\u529b\u3002<\/p>\n<p>\u8fd9\u4e00\u6210\u679c\u7684\u6838\u5fc3\u610f\u4e49\u5728\u4e8e&#xff1a;\u5b83\u5c55\u793a\u4e86\u901a\u7528\u5927\u6a21\u578b\u5728\u6709\u6548\u5f15\u5bfc\u4e0b\u80fd\u591f\u638c\u63e1\u9ad8\u5ea6\u4e13\u4e1a\u5316\u7684\u6280\u80fd&#xff0c;\u6311\u6218\u4e86 \u201c\u9886\u57df\u4e13\u7cbe\u5fc5\u987b\u4f9d\u8d56\u9886\u57df\u6570\u636e\u201d \u7684\u4f20\u7edf\u89c2\u5ff5\u3002\u901a\u8fc7\u53cd\u5c04\u5f0f\u5206\u89e3\u4e0e\u8fed\u4ee3\u4fee\u590d\u7684\u534f\u540c\u5de5\u4f5c&#xff0c;\u4ee5\u53ca\u4e13\u7528 DSL \u7684\u6280\u672f\u652f\u6491&#xff0c;Delta Prover \u6784\u5efa\u4e86\u4e00\u4e2a\u6a21\u62df\u4eba\u7c7b\u95ee\u9898\u89e3\u51b3\u8fc7\u7a0b\u7684 AI \u4ee3\u7406&#xff0c;\u4e3a\u590d\u6742\u63a8\u7406\u4efb\u52a1\u63d0\u4f9b\u4e86\u65b0\u7684\u89e3\u51b3\u65b9\u6848\u3002<\/p>\n<p>\u5c55\u671b\u672a\u6765&#xff0c;Delta Prover \u53ca\u5176\u80cc\u540e\u7684\u8bbe\u8ba1\u7406\u5ff5\u5c06\u63a8\u52a8 AI \u5f62\u5f0f\u5316\u63a8\u7406\u6280\u672f\u5411\u66f4\u5e7f\u6cdb\u7684\u6570\u5b66\u9886\u57df\u6269\u5c55&#xff0c;\u4e3a\u6570\u5b66\u7814\u7a76\u548c\u6559\u80b2\u63d0\u4f9b\u5f3a\u5927\u5de5\u5177\u3002\u540c\u65f6&#xff0c;\u5176\u4ee3\u7406\u67b6\u6784\u601d\u60f3\u5c06\u542f\u53d1\u66f4\u901a\u7528\u7684 AI \u95ee\u9898\u89e3\u51b3\u7cfb\u7edf\u5f00\u53d1&#xff0c;\u63a8\u52a8 AI \u4ece\u4e13\u9879\u80fd\u529b\u5411\u7efc\u5408\u667a\u80fd\u8fc8\u8fdb\u3002<\/p>\n<p>\u5728\u8fd9\u4e2a AI \u5feb\u901f\u53d1\u5c55\u7684\u65f6\u4ee3&#xff0c;Delta Prover \u63d0\u9192\u6211\u4eec&#xff1a;\u6280\u672f\u7a81\u7834\u4e0d\u4ec5\u6765\u81ea\u66f4\u5927\u7684\u6a21\u578b\u548c\u66f4\u591a\u7684\u6570\u636e&#xff0c;\u66f4\u6765\u81ea\u5de7\u5999\u7684\u6846\u67b6\u8bbe\u8ba1\u548c\u5bf9\u95ee\u9898\u672c\u8d28\u7684\u6df1\u523b\u7406\u89e3\u3002\u901a\u8fc7\u6784\u5efa\u80fd\u591f\u5145\u5206\u53d1\u6325\u901a\u7528\u667a\u80fd\u6f5c\u529b\u7684\u7cfb\u7edf&#xff0c;\u6211\u4eec\u6b63\u9010\u6b65\u63a5\u8fd1\u5b9e\u73b0\u771f\u6b63\u7684\u4eba\u5de5\u667a\u80fd\u95ee\u9898\u89e3\u51b3\u8005\u7684\u76ee\u6807&#xff0c;\u8fd9\u4e0d\u4ec5\u5c06\u6539\u53d8\u6570\u5b66\u548c\u8ba1\u7b97\u673a\u79d1\u5b66\u7684\u7814\u7a76\u65b9\u5f0f&#xff0c;\u66f4\u5c06\u63a8\u52a8\u6574\u4e2a\u793e\u4f1a\u7684\u6280\u672f\u8fdb\u6b65\u548c\u521b\u65b0\u3002<\/p>\n","protected":false},"excerpt":{"rendered":"<p>\u6587\u7ae0\u6d4f\u89c8\u9605\u8bfb661\u6b21\uff0c\u70b9\u8d5e17\u6b21\uff0c\u6536\u85cf13\u6b21\u3002\u5728\u4eba\u5de5\u667a\u80fd\u9886\u57df\uff0c\u5f62\u5f0f\u5316\u6570\u5b66\u8bc1\u660e\u957f\u671f\u4ee5\u6765\u88ab\u89c6\u4e3a\u8861\u91cf\u673a\u5668\u63a8\u7406\u80fd\u529b\u7684&quot;\u73e0\u7a46\u6717\u739b\u5cf0&quot;\u3002\u4ece\u53e4\u5e0c\u814a\u51e0\u4f55\u516c\u7406\u5230\u73b0\u4ee3\u6570\u5b66\u7684\u590d\u6742\u5b9a\u7406\uff0c\u4eba\u7c7b\u4f9d\u9760\u903b\u8f91\u6f14\u7ece\u6784\u5efa\u4e86\u5b8f\u4f1f\u7684\u77e5\u8bc6\u5927\u53a6\uff0c\u800c\u8ba9\u673a\u5668\u638c\u63e1\u8fd9\u79cd\u7cbe\u5bc6\u63a8\u7406\u80fd\u529b\u4e00\u76f4\u662fAI\u7814\u7a76\u7684\u6838\u5fc3\u76ee\u6807\u3002\u8fd1\u671f\uff0c\u5b57\u8282\u8df3\u52a8Seed\u56e2\u961f\u53d1\u5e03\u7684Delta Prover\u6846\u67b6\u5728\u8fd9\u4e00\u9886\u57df\u53d6\u5f97\u4e86\u7a81\u7834\u6027\u8fdb\u5c55\u2014\u2014\u65e0\u9700\u4e13\u95e8\u8bad\u7ec3\uff0c\u4ec5\u901a\u8fc7\u901a\u7528\u5927\u6a21\u578b\u4e0eLean 4\u8bc1\u660e\u73af\u5883\u7684\u667a\u80fd\u534f\u4f5c\uff0c\u5c31\u5728miniF2F-test\u57fa\u51c6\u6d4b\u8bd5\u4e2d\u5b9e\u73b0\u4e8695.9%\u7684\u6210\u529f\u7387\uff0c\u8d85\u8d8a\u4e86\u6240\u6709\u9700\u8981\u6a21\u578b\u4e13\u95e8\u5316\u7684\u73b0\u6709\u65b9\u6cd5\u3002<\/p>\n","protected":false},"author":2,"featured_media":51216,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[1],"tags":[5054,50],"topic":[],"class_list":["post-51224","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-server","tag-llm-prover","tag-50"],"yoast_head":"<!-- This site is optimized with the Yoast SEO plugin v20.3 - https:\/\/yoast.com\/wordpress\/plugins\/seo\/ -->\n<title>\u7a81\u7834\u5f62\u5f0f\u5316\u6570\u5b66\u8bc1\u660e\u7684\u8fb9\u754c\uff1a\u5b57\u8282\u8df3\u52a8Delta Prover\u5982\u4f55\u8ba9\u901a\u7528\u5927\u6a21\u578b\u5177\u5907\u9876\u5c16\u5b9a\u7406\u8bc1\u660e\u80fd\u529b - \u7f51\u7855\u4e92\u8054\u5e2e\u52a9\u4e2d\u5fc3<\/title>\n<meta name=\"robots\" content=\"index, follow, max-snippet:-1, max-image-preview:large, max-video-preview:-1\" \/>\n<link rel=\"canonical\" href=\"https:\/\/www.wsisp.com\/helps\/51224.html\" \/>\n<meta property=\"og:locale\" content=\"zh_CN\" \/>\n<meta property=\"og:type\" content=\"article\" \/>\n<meta property=\"og:title\" content=\"\u7a81\u7834\u5f62\u5f0f\u5316\u6570\u5b66\u8bc1\u660e\u7684\u8fb9\u754c\uff1a\u5b57\u8282\u8df3\u52a8Delta Prover\u5982\u4f55\u8ba9\u901a\u7528\u5927\u6a21\u578b\u5177\u5907\u9876\u5c16\u5b9a\u7406\u8bc1\u660e\u80fd\u529b - \u7f51\u7855\u4e92\u8054\u5e2e\u52a9\u4e2d\u5fc3\" \/>\n<meta property=\"og:description\" content=\"\u6587\u7ae0\u6d4f\u89c8\u9605\u8bfb661\u6b21\uff0c\u70b9\u8d5e17\u6b21\uff0c\u6536\u85cf13\u6b21\u3002\u5728\u4eba\u5de5\u667a\u80fd\u9886\u57df\uff0c\u5f62\u5f0f\u5316\u6570\u5b66\u8bc1\u660e\u957f\u671f\u4ee5\u6765\u88ab\u89c6\u4e3a\u8861\u91cf\u673a\u5668\u63a8\u7406\u80fd\u529b\u7684&quot;\u73e0\u7a46\u6717\u739b\u5cf0&quot;\u3002\u4ece\u53e4\u5e0c\u814a\u51e0\u4f55\u516c\u7406\u5230\u73b0\u4ee3\u6570\u5b66\u7684\u590d\u6742\u5b9a\u7406\uff0c\u4eba\u7c7b\u4f9d\u9760\u903b\u8f91\u6f14\u7ece\u6784\u5efa\u4e86\u5b8f\u4f1f\u7684\u77e5\u8bc6\u5927\u53a6\uff0c\u800c\u8ba9\u673a\u5668\u638c\u63e1\u8fd9\u79cd\u7cbe\u5bc6\u63a8\u7406\u80fd\u529b\u4e00\u76f4\u662fAI\u7814\u7a76\u7684\u6838\u5fc3\u76ee\u6807\u3002\u8fd1\u671f\uff0c\u5b57\u8282\u8df3\u52a8Seed\u56e2\u961f\u53d1\u5e03\u7684Delta Prover\u6846\u67b6\u5728\u8fd9\u4e00\u9886\u57df\u53d6\u5f97\u4e86\u7a81\u7834\u6027\u8fdb\u5c55\u2014\u2014\u65e0\u9700\u4e13\u95e8\u8bad\u7ec3\uff0c\u4ec5\u901a\u8fc7\u901a\u7528\u5927\u6a21\u578b\u4e0eLean 4\u8bc1\u660e\u73af\u5883\u7684\u667a\u80fd\u534f\u4f5c\uff0c\u5c31\u5728miniF2F-test\u57fa\u51c6\u6d4b\u8bd5\u4e2d\u5b9e\u73b0\u4e8695.9%\u7684\u6210\u529f\u7387\uff0c\u8d85\u8d8a\u4e86\u6240\u6709\u9700\u8981\u6a21\u578b\u4e13\u95e8\u5316\u7684\u73b0\u6709\u65b9\u6cd5\u3002\" \/>\n<meta property=\"og:url\" content=\"https:\/\/www.wsisp.com\/helps\/51224.html\" \/>\n<meta property=\"og:site_name\" content=\"\u7f51\u7855\u4e92\u8054\u5e2e\u52a9\u4e2d\u5fc3\" \/>\n<meta property=\"article:published_time\" content=\"2025-08-10T11:14:57+00:00\" \/>\n<meta property=\"og:image\" content=\"https:\/\/www.wsisp.com\/helps\/wp-content\/uploads\/2025\/08\/20250810111441-68987f210bf85.png\" \/>\n<meta name=\"author\" content=\"admin\" \/>\n<meta name=\"twitter:card\" content=\"summary_large_image\" \/>\n<meta name=\"twitter:label1\" content=\"\u4f5c\u8005\" \/>\n\t<meta name=\"twitter:data1\" content=\"admin\" \/>\n\t<meta name=\"twitter:label2\" content=\"\u9884\u8ba1\u9605\u8bfb\u65f6\u95f4\" \/>\n\t<meta name=\"twitter:data2\" content=\"5 \u5206\" \/>\n<script type=\"application\/ld+json\" class=\"yoast-schema-graph\">{\"@context\":\"https:\/\/schema.org\",\"@graph\":[{\"@type\":\"WebPage\",\"@id\":\"https:\/\/www.wsisp.com\/helps\/51224.html\",\"url\":\"https:\/\/www.wsisp.com\/helps\/51224.html\",\"name\":\"\u7a81\u7834\u5f62\u5f0f\u5316\u6570\u5b66\u8bc1\u660e\u7684\u8fb9\u754c\uff1a\u5b57\u8282\u8df3\u52a8Delta Prover\u5982\u4f55\u8ba9\u901a\u7528\u5927\u6a21\u578b\u5177\u5907\u9876\u5c16\u5b9a\u7406\u8bc1\u660e\u80fd\u529b - \u7f51\u7855\u4e92\u8054\u5e2e\u52a9\u4e2d\u5fc3\",\"isPartOf\":{\"@id\":\"https:\/\/www.wsisp.com\/helps\/#website\"},\"datePublished\":\"2025-08-10T11:14:57+00:00\",\"dateModified\":\"2025-08-10T11:14:57+00:00\",\"author\":{\"@id\":\"https:\/\/www.wsisp.com\/helps\/#\/schema\/person\/358e386c577a3ab51c4493330a20ad41\"},\"breadcrumb\":{\"@id\":\"https:\/\/www.wsisp.com\/helps\/51224.html#breadcrumb\"},\"inLanguage\":\"zh-Hans\",\"potentialAction\":[{\"@type\":\"ReadAction\",\"target\":[\"https:\/\/www.wsisp.com\/helps\/51224.html\"]}]},{\"@type\":\"BreadcrumbList\",\"@id\":\"https:\/\/www.wsisp.com\/helps\/51224.html#breadcrumb\",\"itemListElement\":[{\"@type\":\"ListItem\",\"position\":1,\"name\":\"\u9996\u9875\",\"item\":\"https:\/\/www.wsisp.com\/helps\"},{\"@type\":\"ListItem\",\"position\":2,\"name\":\"\u7a81\u7834\u5f62\u5f0f\u5316\u6570\u5b66\u8bc1\u660e\u7684\u8fb9\u754c\uff1a\u5b57\u8282\u8df3\u52a8Delta Prover\u5982\u4f55\u8ba9\u901a\u7528\u5927\u6a21\u578b\u5177\u5907\u9876\u5c16\u5b9a\u7406\u8bc1\u660e\u80fd\u529b\"}]},{\"@type\":\"WebSite\",\"@id\":\"https:\/\/www.wsisp.com\/helps\/#website\",\"url\":\"https:\/\/www.wsisp.com\/helps\/\",\"name\":\"\u7f51\u7855\u4e92\u8054\u5e2e\u52a9\u4e2d\u5fc3\",\"description\":\"\u9999\u6e2f\u670d\u52a1\u5668_\u9999\u6e2f\u4e91\u670d\u52a1\u5668\u8d44\u8baf_\u670d\u52a1\u5668\u5e2e\u52a9\u6587\u6863_\u670d\u52a1\u5668\u6559\u7a0b\",\"potentialAction\":[{\"@type\":\"SearchAction\",\"target\":{\"@type\":\"EntryPoint\",\"urlTemplate\":\"https:\/\/www.wsisp.com\/helps\/?s={search_term_string}\"},\"query-input\":\"required name=search_term_string\"}],\"inLanguage\":\"zh-Hans\"},{\"@type\":\"Person\",\"@id\":\"https:\/\/www.wsisp.com\/helps\/#\/schema\/person\/358e386c577a3ab51c4493330a20ad41\",\"name\":\"admin\",\"image\":{\"@type\":\"ImageObject\",\"inLanguage\":\"zh-Hans\",\"@id\":\"https:\/\/www.wsisp.com\/helps\/#\/schema\/person\/image\/\",\"url\":\"https:\/\/gravatar.wp-china-yes.net\/avatar\/?s=96&d=mystery\",\"contentUrl\":\"https:\/\/gravatar.wp-china-yes.net\/avatar\/?s=96&d=mystery\",\"caption\":\"admin\"},\"sameAs\":[\"http:\/\/wp.wsisp.com\"],\"url\":\"https:\/\/www.wsisp.com\/helps\/author\/admin\"}]}<\/script>\n<!-- \/ Yoast SEO plugin. -->","yoast_head_json":{"title":"\u7a81\u7834\u5f62\u5f0f\u5316\u6570\u5b66\u8bc1\u660e\u7684\u8fb9\u754c\uff1a\u5b57\u8282\u8df3\u52a8Delta Prover\u5982\u4f55\u8ba9\u901a\u7528\u5927\u6a21\u578b\u5177\u5907\u9876\u5c16\u5b9a\u7406\u8bc1\u660e\u80fd\u529b - \u7f51\u7855\u4e92\u8054\u5e2e\u52a9\u4e2d\u5fc3","robots":{"index":"index","follow":"follow","max-snippet":"max-snippet:-1","max-image-preview":"max-image-preview:large","max-video-preview":"max-video-preview:-1"},"canonical":"https:\/\/www.wsisp.com\/helps\/51224.html","og_locale":"zh_CN","og_type":"article","og_title":"\u7a81\u7834\u5f62\u5f0f\u5316\u6570\u5b66\u8bc1\u660e\u7684\u8fb9\u754c\uff1a\u5b57\u8282\u8df3\u52a8Delta Prover\u5982\u4f55\u8ba9\u901a\u7528\u5927\u6a21\u578b\u5177\u5907\u9876\u5c16\u5b9a\u7406\u8bc1\u660e\u80fd\u529b - \u7f51\u7855\u4e92\u8054\u5e2e\u52a9\u4e2d\u5fc3","og_description":"\u6587\u7ae0\u6d4f\u89c8\u9605\u8bfb661\u6b21\uff0c\u70b9\u8d5e17\u6b21\uff0c\u6536\u85cf13\u6b21\u3002\u5728\u4eba\u5de5\u667a\u80fd\u9886\u57df\uff0c\u5f62\u5f0f\u5316\u6570\u5b66\u8bc1\u660e\u957f\u671f\u4ee5\u6765\u88ab\u89c6\u4e3a\u8861\u91cf\u673a\u5668\u63a8\u7406\u80fd\u529b\u7684&quot;\u73e0\u7a46\u6717\u739b\u5cf0&quot;\u3002\u4ece\u53e4\u5e0c\u814a\u51e0\u4f55\u516c\u7406\u5230\u73b0\u4ee3\u6570\u5b66\u7684\u590d\u6742\u5b9a\u7406\uff0c\u4eba\u7c7b\u4f9d\u9760\u903b\u8f91\u6f14\u7ece\u6784\u5efa\u4e86\u5b8f\u4f1f\u7684\u77e5\u8bc6\u5927\u53a6\uff0c\u800c\u8ba9\u673a\u5668\u638c\u63e1\u8fd9\u79cd\u7cbe\u5bc6\u63a8\u7406\u80fd\u529b\u4e00\u76f4\u662fAI\u7814\u7a76\u7684\u6838\u5fc3\u76ee\u6807\u3002\u8fd1\u671f\uff0c\u5b57\u8282\u8df3\u52a8Seed\u56e2\u961f\u53d1\u5e03\u7684Delta Prover\u6846\u67b6\u5728\u8fd9\u4e00\u9886\u57df\u53d6\u5f97\u4e86\u7a81\u7834\u6027\u8fdb\u5c55\u2014\u2014\u65e0\u9700\u4e13\u95e8\u8bad\u7ec3\uff0c\u4ec5\u901a\u8fc7\u901a\u7528\u5927\u6a21\u578b\u4e0eLean 4\u8bc1\u660e\u73af\u5883\u7684\u667a\u80fd\u534f\u4f5c\uff0c\u5c31\u5728miniF2F-test\u57fa\u51c6\u6d4b\u8bd5\u4e2d\u5b9e\u73b0\u4e8695.9%\u7684\u6210\u529f\u7387\uff0c\u8d85\u8d8a\u4e86\u6240\u6709\u9700\u8981\u6a21\u578b\u4e13\u95e8\u5316\u7684\u73b0\u6709\u65b9\u6cd5\u3002","og_url":"https:\/\/www.wsisp.com\/helps\/51224.html","og_site_name":"\u7f51\u7855\u4e92\u8054\u5e2e\u52a9\u4e2d\u5fc3","article_published_time":"2025-08-10T11:14:57+00:00","og_image":[{"url":"https:\/\/www.wsisp.com\/helps\/wp-content\/uploads\/2025\/08\/20250810111441-68987f210bf85.png"}],"author":"admin","twitter_card":"summary_large_image","twitter_misc":{"\u4f5c\u8005":"admin","\u9884\u8ba1\u9605\u8bfb\u65f6\u95f4":"5 \u5206"},"schema":{"@context":"https:\/\/schema.org","@graph":[{"@type":"WebPage","@id":"https:\/\/www.wsisp.com\/helps\/51224.html","url":"https:\/\/www.wsisp.com\/helps\/51224.html","name":"\u7a81\u7834\u5f62\u5f0f\u5316\u6570\u5b66\u8bc1\u660e\u7684\u8fb9\u754c\uff1a\u5b57\u8282\u8df3\u52a8Delta Prover\u5982\u4f55\u8ba9\u901a\u7528\u5927\u6a21\u578b\u5177\u5907\u9876\u5c16\u5b9a\u7406\u8bc1\u660e\u80fd\u529b - \u7f51\u7855\u4e92\u8054\u5e2e\u52a9\u4e2d\u5fc3","isPartOf":{"@id":"https:\/\/www.wsisp.com\/helps\/#website"},"datePublished":"2025-08-10T11:14:57+00:00","dateModified":"2025-08-10T11:14:57+00:00","author":{"@id":"https:\/\/www.wsisp.com\/helps\/#\/schema\/person\/358e386c577a3ab51c4493330a20ad41"},"breadcrumb":{"@id":"https:\/\/www.wsisp.com\/helps\/51224.html#breadcrumb"},"inLanguage":"zh-Hans","potentialAction":[{"@type":"ReadAction","target":["https:\/\/www.wsisp.com\/helps\/51224.html"]}]},{"@type":"BreadcrumbList","@id":"https:\/\/www.wsisp.com\/helps\/51224.html#breadcrumb","itemListElement":[{"@type":"ListItem","position":1,"name":"\u9996\u9875","item":"https:\/\/www.wsisp.com\/helps"},{"@type":"ListItem","position":2,"name":"\u7a81\u7834\u5f62\u5f0f\u5316\u6570\u5b66\u8bc1\u660e\u7684\u8fb9\u754c\uff1a\u5b57\u8282\u8df3\u52a8Delta Prover\u5982\u4f55\u8ba9\u901a\u7528\u5927\u6a21\u578b\u5177\u5907\u9876\u5c16\u5b9a\u7406\u8bc1\u660e\u80fd\u529b"}]},{"@type":"WebSite","@id":"https:\/\/www.wsisp.com\/helps\/#website","url":"https:\/\/www.wsisp.com\/helps\/","name":"\u7f51\u7855\u4e92\u8054\u5e2e\u52a9\u4e2d\u5fc3","description":"\u9999\u6e2f\u670d\u52a1\u5668_\u9999\u6e2f\u4e91\u670d\u52a1\u5668\u8d44\u8baf_\u670d\u52a1\u5668\u5e2e\u52a9\u6587\u6863_\u670d\u52a1\u5668\u6559\u7a0b","potentialAction":[{"@type":"SearchAction","target":{"@type":"EntryPoint","urlTemplate":"https:\/\/www.wsisp.com\/helps\/?s={search_term_string}"},"query-input":"required name=search_term_string"}],"inLanguage":"zh-Hans"},{"@type":"Person","@id":"https:\/\/www.wsisp.com\/helps\/#\/schema\/person\/358e386c577a3ab51c4493330a20ad41","name":"admin","image":{"@type":"ImageObject","inLanguage":"zh-Hans","@id":"https:\/\/www.wsisp.com\/helps\/#\/schema\/person\/image\/","url":"https:\/\/gravatar.wp-china-yes.net\/avatar\/?s=96&d=mystery","contentUrl":"https:\/\/gravatar.wp-china-yes.net\/avatar\/?s=96&d=mystery","caption":"admin"},"sameAs":["http:\/\/wp.wsisp.com"],"url":"https:\/\/www.wsisp.com\/helps\/author\/admin"}]}},"_links":{"self":[{"href":"https:\/\/www.wsisp.com\/helps\/wp-json\/wp\/v2\/posts\/51224","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/www.wsisp.com\/helps\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.wsisp.com\/helps\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.wsisp.com\/helps\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.wsisp.com\/helps\/wp-json\/wp\/v2\/comments?post=51224"}],"version-history":[{"count":0,"href":"https:\/\/www.wsisp.com\/helps\/wp-json\/wp\/v2\/posts\/51224\/revisions"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/www.wsisp.com\/helps\/wp-json\/wp\/v2\/media\/51216"}],"wp:attachment":[{"href":"https:\/\/www.wsisp.com\/helps\/wp-json\/wp\/v2\/media?parent=51224"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.wsisp.com\/helps\/wp-json\/wp\/v2\/categories?post=51224"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.wsisp.com\/helps\/wp-json\/wp\/v2\/tags?post=51224"},{"taxonomy":"topic","embeddable":true,"href":"https:\/\/www.wsisp.com\/helps\/wp-json\/wp\/v2\/topic?post=51224"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}