{"id":821311,"date":"2026-08-02T15:33:15","date_gmt":"2026-08-02T07:33:15","guid":{"rendered":"https:\/\/www.alphaseek.cn\/?p=821311"},"modified":"2026-08-02T15:33:15","modified_gmt":"2026-08-02T07:33:15","slug":"openai%e7%94%a8%e6%96%b0%e6%a8%a1%e5%9e%8bastra%e4%b8%80%e6%ac%a1%e5%81%9a%e5%87%ba%e5%8d%81%e9%a1%b9%e6%95%b0%e5%ad%a6%e6%96%b0%e7%bb%93%e6%9e%9c%ef%bc%8ctoken%e8%8a%b1%e4%ba%862000%e7%be%8e%e5%85%83","status":"publish","type":"post","link":"https:\/\/www.alphaseek.cn\/?p=821311","title":{"rendered":"OpenAI\u7528\u65b0\u6a21\u578bAstra\u4e00\u6b21\u505a\u51fa\u5341\u9879\u6570\u5b66\u65b0\u7ed3\u679c\uff0ctoken\u82b1\u4e862000\u7f8e\u5143"},"content":{"rendered":"

8\u67082\u65e5\u6d88\u606f\uff0cOpenAI<\/a>\u5468\u516d\u516c\u5f00\u5341\u9879\u6570\u5b66<\/a>\u4e0e\u7406\u8bba\u8ba1\u7b97\u673a\u79d1\u5b66\u6210\u679c\uff0c\u540c\u65f6\u653e\u51fa249\u9875\u8bba\u6587\u300162\u9875\u63a8\u7406\u8bf4\u660e\u548c\u4e00\u5957Lean 4\u5f62\u5f0f\u5316\u8bc1\u660e\u3002\u4e0d\u8fc7\u751f\u6210\u8fd9\u4e9b\u7ed3\u679c\u7684\u4e0b\u4e00\u4ee3\u6a21\u578bAstra<\/a>\u4ecd\u662f\u5185\u90e8\u7248\u672c\uff0c\u6ca1\u6709\u968f\u4e4b\u5f00\u653e\u3002<\/p>\n

\u636eOpenAI<\/a>\u4ecb\u7ecd\uff0cAstra\u751f\u6210\u6570\u5b66\u8bba\u8bc1\u540e\uff0c\u4eba\u7c7b\u4e0e\u6a21\u578b\u5171\u540c\u5c06\u5176\u6574\u7406\u6210\u8bba\u6587\uff0c\u518d\u7531\u6a21\u578b\u7f16\u5199Lean\u8bc1\u660e\u3002OpenAI\u628a\u5bfb\u627e\u5341\u9879\u89e3\u6cd5\u6d88\u8017\u7684token<\/a>\u6309Sol API\u4ef7\u683c\u6298\u7b97\uff0c\u4f30\u8ba1\u6210\u672c\u7ea6\u4e3a2000\u7f8e\u5143\u3002<\/p>\n

\u8fd9\u79cd\u53d1\u5e03\u65b9\u5f0f\u5728AI\u884c\u4e1a\u91cc\u4e0d\u592a\u5bfb\u5e38\u7684\uff1a\u5916\u754c\u6682\u65f6\u65e0\u6cd5\u6d4b\u8bd5Astra\uff0c\u5374\u53ef\u4ee5\u5148\u68c0\u67e5\u5b83\u4ea4\u51fa\u7684\u6570\u5b66\u7ed3\u679c\u3002<\/p>\n

\u5468\u4e94The Information\u66fe\u63f4\u5f15\u4e09\u540d\u77e5\u60c5\u4eba\u58eb\u79f0\uff0cAstra\u5f53\u65f6\u4ecd\u662f\u6682\u5b9a\u540d\u79f0\u3002OpenAI\u5411\u534e\u76db\u987f\u7684\u653f\u7b56\u5236\u5b9a\u8005\u548c\u76d1\u7ba1\u4eba\u5458\u6f14\u793a\u8fc7\u5b83\u5904\u7406\u957f\u65f6\u4efb\u52a1\u548c\u591a\u667a\u80fd\u4f53\u534f\u4f5c\u7684\u80fd\u529b\uff0c\u4f46\u6ca1\u6709\u7ed9\u51fa\u4ea7\u54c1\u53d1\u5e03\u65f6\u95f4\u548c\u6700\u7ec8\u578b\u53f7\u3002<\/p>\n

\u5341\u9879\u6210\u679c\uff0c\u5206\u5c5e\u4e0d\u540c\u7684\u8bc1\u660e\u4efb\u52a1<\/b><\/p>\n

\u8fd9\u4efd\u540d\u5355\u6a2a\u8de8\u9ad8\u7ef4\u51e0\u4f55\u3001\u7f16\u7801\u7406\u8bba\u3001\u7fa4\u8bba\u3001\u7b97\u672f\u7535\u8def\u3001\u91cf\u5b50\u590d\u6742\u6027\u3001\u683c\u5bc6\u7801\u548c\u6781\u503c\u7ec4\u5408\u6570\u5b66\u7b49\u591a\u4e2a\u5206\u652f\u3002<\/p>\n

\u5177\u4f53\u6765\u770b\uff0c\u9ad8\u7ef4\u7403\u5806\u79ef\u548c\u7f16\u7801\u7406\u8bba\u5f97\u5230\u65b0\u7684\u4e0a\u754c\uff1bAstra\u6784\u9020\u4e86\u975esofic\u7fa4\uff0c\u5e76\u4e3aConnes\u521a\u6027\u731c\u60f3\u7ed9\u51fa\u53cd\u4f8b\uff1bEhrhart\u4f53\u79ef\u731c\u60f3\u5f97\u5230\u9510\u754c\uff1b\u591a\u8272Ramsey\u6570\u548c\u6781\u503c\u56fe\u8bba\u7684\u7814\u7a76\u5219\u89e3\u51b3\u4e86\u4e09\u4e2a\u7531\u4fdd\u7f57\u00b7\u5384\u591a\u65af\u63d0\u51fa\u3001\u957f\u671f\u672a\u89e3\u7684\u95ee\u9898\u3002<\/p>\n

\u6709\u4e9b\u5de5\u4f5c\u628a\u5df2\u77e5\u8fb9\u754c\u5411\u524d\u63a8\u8fdb\uff0c\u6709\u4e9b\u6784\u9020\u8fc7\u53bb\u4e0d\u77e5\u9053\u662f\u5426\u5b58\u5728\u7684\u5bf9\u8c61\uff0c\u8fd8\u6709\u4e9b\u63a8\u7ffb\u6216\u5b8c\u6210\u5177\u4f53\u731c\u60f3\u3002\u5b83\u4eec\u88ab\u653e\u5728\u540c\u4e00\u6b21\u53d1\u5e03\u91cc\uff0c\u540e\u7eed\u590d\u6838\u548c\u5f15\u7528\u5219\u4f1a\u5206\u522b\u53d1\u751f\u5728\u5404\u81ea\u9886\u57df\u3002<\/p>\n

Lean <\/b>\u7ed9\u5916\u90e8\u590d\u6838\u52a0\u4e86\u4e00\u6761\u53ef\u8fd0\u884c\u8def\u5f84<\/b><\/p>\n

OpenAI\u5728GitHub\u516c\u5e03\u4e86\u5341\u9879\u7ed3\u679c\u7684Lean\u6587\u4ef6\u3001\u7edf\u4e00\u6784\u5efa\u547d\u4ee4\u548cComparator\u914d\u7f6e\u3002\u5b98\u65b9\u5f62\u5f0f\u5316\u6e05\u5355\u663e\u793a\uff0c\u4e3b\u8981\u8bc1\u660e\u7684sorry_count\u4e3a0\uff0c\u53ea\u4f7f\u7528propext\u3001Classical.choice\u548cQuot.sound\u4e09\u7c7b\u516c\u7406\u3002Comparator\u76ee\u5f55\u91cc\u7684sorry\u662f\u7559\u7ed9\u5916\u90e8\u6838\u9a8c\u8005\u7684\u9898\u9762\u7a7a\u7f3a\uff0c\u4e0d\u5728\u6b63\u5f0f\u8bc1\u660e\u6587\u4ef6\u4e2d\u3002<\/p>\n

\u914d\u7f6e\u76f8\u5e94\u7248\u672c\u7684Lean\u3001mathlib\u548cComparator\u540e\uff0c\u7814\u7a76\u8005\u53ef\u4ee5\u5728\u672c\u5730\u91cd\u8dd1\u8bc1\u660e\uff0c\u68c0\u67e5\u89e3\u7b54\u662f\u5426\u8bc1\u660e\u540c\u4e00\u5f62\u5f0f\u5316\u547d\u9898\u3001\u662f\u5426\u5f15\u5165\u6e05\u5355\u4e4b\u5916\u7684\u516c\u7406\u3001\u4ee5\u53ca\u63a8\u5bfc\u80fd\u5426\u88abLean\u5185\u6838\u63a5\u53d7\u3002\u540c\u884c\u5ba1\u7a3f\u901a\u5e38\u9700\u8981\u6570\u6708\u4e43\u81f3\u6570\u5e74\uff0c\u5f62\u5f0f\u5316\u6587\u4ef6\u63d0\u4f9b\u4e86\u4e00\u6761\u53ef\u4ee5\u5b9a\u4f4d\u5230\u5177\u4f53\u884c\u7684\u590d\u6838\u8def\u5f84\u3002<\/p>\n

\u4e0d\u8fc7Lean\u5185\u6838\u53ea\u68c0\u67e5\u63a8\u5bfc\u672c\u8eab\u3002\u731c\u60f3\u5230\u5f62\u5f0f\u5316\u547d\u9898\u7684\u7ffb\u8bd1\u662f\u5426\u8d70\u6837\u3001\u65b9\u6cd5\u662f\u5426\u65b0\u9896\u3001\u7ed3\u679c\u5728\u5b66\u79d1\u5185\u7684\u5206\u91cf\uff0c\u4ecd\u9700\u8981\u4eba\u6765\u5224\u65ad\u3002<\/p>\n<\/p>\n

62\u9875\u63a8\u7406\u8bf4\u660e\u662f\u4e8b\u540e\u6574\u7406\u7a3f\u3002\u6587\u4ef6\u6ce8\u660e\uff0c\u6a21\u578b\u8bfb\u8fc7\u539f\u59cb\u601d\u7ef4\u94fe\u4e0e\u6700\u7ec8\u8bba\u6587\u540e\uff0c\u91cd\u65b0\u53d9\u8ff0\u6210\u529f\u601d\u8def\u3001\u5931\u8d25\u8def\u7ebf\u548c\u8f6c\u6298\u70b9\u3002\u8fd9\u610f\u5473\u7740\uff0c\u8bfb\u8005\u770b\u5230\u7684\u662f\u91cd\u6784\u540e\u7684\u8def\u7ebf\u56fe\uff0c\u4e0d\u662f\u6a21\u578b\u5f53\u65f6\u7684\u539f\u59cb\u601d\u8003\u3002<\/p>\n

2000 <\/b>\u7f8e\u5143\u53ea\u662f<\/b> token <\/b>\u6210\u672c<\/b><\/p>\n

\u5bfb\u627e\u89e3\u6cd5\u7ea62000\u7f8e\u5143\u8fd9\u4e2a\u6570\u5b57\uff0c\u53ea\u8ba1\u7b97token\uff0c\u5e76\u6309Sol API\u4ef7\u683c\u6298\u7b97\u3002\u6a21\u578b\u8bad\u7ec3\u3001\u9009\u9898\u3001\u6570\u5b66\u5bb6\u53c2\u4e0e\u3001\u57fa\u7840\u8bbe\u65bd\u548c\u9879\u76ee\u4e2d\u7684\u5176\u4ed6\u6210\u672c\u6ca1\u6709\u5217\u5165\u3002\u5b98\u65b9\u4ed3\u5e93\u53e6\u6ce8\u660e\uff0c\u628a\u8fd9\u4e9b\u8bc1\u660e\u5199\u6210Lean\u5f62\u5f0f\u5316\u6587\u4ef6\uff0c\u524d\u540e\u82b1\u4e86\u4e00\u5468\u65f6\u95f4\u3002<\/p>\n

\u4e0e\u8fd9\u6b21\u53d1\u5e03\u540c\u671f\uff0c\u300a\u534e\u5c14\u8857<\/a>\u65e5\u62a5\u300b\u62a5\u9053\uff0c\u65b0\u664b\u83f2\u5c14\u5179\u5956\u5f97\u4e3b\u96c5\u5404\u5e03\u00b7\u9f50\u9ed8\u66fc\uff08Jacob Tsimerman\uff09\u5c06\u4ece\u591a\u4f26\u591a\u5927\u5b66\u4f11\u5047\uff0c\u52a0\u5165OpenAI\u4ece\u4e8bAI\u5b89\u5168\u7814\u7a76\u3002\u4ed6\u51c6\u5907\u628a\u6570\u5b66\u4e2d\u7684\u5f62\u5f0f\u8bed\u8a00\u548c\u9a8c\u8bc1\u65b9\u6cd5\u7528\u4e8e\u7406\u89e3\u3001\u8bc4\u4f30\u6a21\u578b\u884c\u4e3a\u3002<\/p>\n

\u4e24\u5468\u524d\uff0cAnthropic\u7814\u7a76\u5458\u83b1\u6587\u7279\u00b7\u963f\u5c14\u73c0\u683c\uff08Levent Alp\u00f6ge\uff09\u516c\u5e03\u4e86Jacobian\u731c\u60f3\u5728\u4e09\u7ef4\u53ca\u66f4\u9ad8\u7ef4\u5ea6\u7684\u53cd\u4f8b\uff0c\u5e76\u628a\u5bfb\u627e\u53cd\u4f8b\u7684\u529f\u52b3\u5f52\u7ed9Fable 5\u3002\u63d0\u793a\u8bcd\u3001\u641c\u7d22\u8fc7\u7a0b\u4ee5\u53ca\u4eba\u548c\u6a21\u578b\u5404\u81ea\u5b8c\u6210\u4e86\u591a\u5c11\u5de5\u4f5c\uff0c\u81f3\u4eca\u6ca1\u6709\u516c\u5f00\u3002<\/p>\n

\u963f\u5c14\u73c0\u683c\u7684\u535a\u58eb\u5bfc\u5e08\u6b63\u662f\u9f50\u9ed8\u66fc\u3002<\/p>\n

OpenAI\u8fd9\u6b21\u7528Lean\u68c0\u67e5\u6a21\u578b\u7ed9\u51fa\u7684\u6570\u5b66\u8bc1\u660e\u3002\u9f50\u9ed8\u66fc\u52a0\u5165\u540e\uff0c\u60f3\u628a\u5f62\u5f0f\u5316\u65b9\u6cd5\u7ee7\u7eed\u7528\u5230\u6a21\u578b\u884c\u4e3a\u4e0a\u3002\u5bf9OpenAI\u800c\u8a00\uff0c\u201c\u9a8c\u8bc1\u201d\u6b63\u5728\u540c\u65f6\u8fdb\u5165\u6a21\u578b\u7684\u4ea7\u51fa\u548c\u6a21\u578b\u672c\u8eab\u3002\uff08\u6613\u53e5\uff09<\/p>\n

\uff08\u672c\u6587\u7531AI\u7ffb\u8bd1\uff0c\u7f51\u6613\u7f16\u8f91\u8d1f\u8d23\u6821\u5bf9\uff09<\/p>\n

(\u6765\u6e90\uff1a\u7f51\u6613\u79d1\u6280) <\/p>\n

<\/div>\n","protected":false},"excerpt":{"rendered":"

8\u67082\u65e5\u6d88\u606f\uff0cOpenAI\u5468\u516d\u516c\u5f00\u5341\u9879\u6570\u5b66\u4e0e\u7406\u8bba\u8ba1\u7b97\u673a\u79d1\u5b66\u6210\u679c\uff0c\u540c\u65f6\u653e\u51fa249\u9875\u8bba\u6587\u300162\u9875\u63a8\u7406\u8bf4\u660e\u548c\u4e00\u5957Le […]<\/p>\n","protected":false},"author":1,"featured_media":0,"comment_status":"closed","ping_status":"closed","sticky":false,"template":"","format":"aside","meta":[],"categories":[6],"tags":[378,142],"views":14,"_links":{"self":[{"href":"https:\/\/www.alphaseek.cn\/index.php?rest_route=\/wp\/v2\/posts\/821311"}],"collection":[{"href":"https:\/\/www.alphaseek.cn\/index.php?rest_route=\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.alphaseek.cn\/index.php?rest_route=\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.alphaseek.cn\/index.php?rest_route=\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/www.alphaseek.cn\/index.php?rest_route=%2Fwp%2Fv2%2Fcomments&post=821311"}],"version-history":[{"count":0,"href":"https:\/\/www.alphaseek.cn\/index.php?rest_route=\/wp\/v2\/posts\/821311\/revisions"}],"wp:attachment":[{"href":"https:\/\/www.alphaseek.cn\/index.php?rest_route=%2Fwp%2Fv2%2Fmedia&parent=821311"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.alphaseek.cn\/index.php?rest_route=%2Fwp%2Fv2%2Fcategories&post=821311"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.alphaseek.cn\/index.php?rest_route=%2Fwp%2Fv2%2Ftags&post=821311"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}