{"id":19670,"date":"2026-09-09T15:45:05","date_gmt":"2026-09-09T05:45:05","guid":{"rendered":"https:\/\/geoffreychen.com\/ai-philosophy-observation-formal-verification-is-not-mathematical-knowledge\/"},"modified":"2026-09-09T15:45:05","modified_gmt":"2026-09-09T05:45:05","slug":"ai-philosophy-observation-formal-verification-is-not-mathematical-knowledge","status":"publish","type":"post","link":"https:\/\/geoffreychen.com\/zh\/ai-philosophy-observation-formal-verification-is-not-mathematical-knowledge\/","title":{"rendered":"AI\u54f2\u5b66\u89c2\u5bdf\uff5c\u5f62\u5f0f\u9a8c\u8bc1\u901a\u8fc7\u4e0d\u7b49\u4e8e\u6570\u5b66\u77e5\u8bc6\u5df2\u7ecf\u786e\u7acb"},"content":{"rendered":"<\/p>\n

2026\u5e749\u67088\u65e5\uff0cOpenAI\u516c\u5f00\u4e86\u4e00\u4efd166\u9875\u7684Navier\u2013Stokes\u6709\u9650\u65f6\u95f4\u5947\u6027\u8bc1\u660e\u7a3f\u548c\u914d\u5957\u7684Lean 4\u5f62\u5f0f\u5316\u4ed3\u5e93\u3002\u8bc1\u660e\u7a3f\u58f0\u79f0\uff1a\u5bf9\u4efb\u610f\u6b63\u9ecf\u5ea6\uff0c\u90fd\u53ef\u4ee5\u6784\u9020\u4ece\u9759\u6b62\u5f00\u59cb\u3001\u53d7\u5149\u6ed1\u5916\u529b\u4f5c\u7528\u7684\u4e09\u7ef4\u4e0d\u53ef\u538b\u7f29\u6d41\u4f53\uff0c\u4f7f\u901f\u5ea6\u5728\u6709\u9650\u65f6\u95f4\u5185\u65e0\u754c\uff0c\u540c\u65f6\u52a8\u80fd\u4fdd\u6301\u6709\u754c\uff1b\u4f5c\u8005\u636e\u6b64\u8ba4\u4e3a\u81ea\u5df1\u5efa\u7acb\u4e86Clay\u6570\u5b66\u7814\u7a76\u6240\u6b63\u5f0f\u95ee\u9898\u8bf4\u660e\u4e2d\u7684C\u548cD\u4e24\u79cd\u201c\u5931\u6548\u201d\u60c5\u5f62\u3002OpenAI\u8fd8\u62a5\u544a\uff0c\u7ea6\u4e00\u4e07\u4e2a\u5e76\u884c\u667a\u80fd\u4f53\u752888\u5c0f\u65f6\u5f97\u5230\u7ed3\u679c\uff0cGPT-6 Astra\u53c8\u752817\u5c0f\u65f6\u5b8c\u6210Lean\u5f62\u5f0f\u5316\u3002\u72ec\u7acb\u62a5\u9053\u786e\u8ba4\u4e86\u6750\u6599\u516c\u5f00\u548c\u8fd9\u4e9b\u5f00\u53d1\u8005\u6570\u636e\uff0c\u4f46\u6ca1\u6709\u786e\u8ba4\u5b9a\u7406\u5df2\u7ecf\u88ab\u6570\u5b66\u754c\u6216Clay\u63a5\u53d7\u3002\u4ed3\u5e93\u5143\u6570\u636e\u628a\u5ba1\u67e5\u72b6\u6001\u5199\u4e3a\u201cself-assessed\u201d\uff0c\u622a\u81f3\u672c\u6587\u5199\u4f5c\u65f6\u4e5f\u6ca1\u6709\u516c\u5f00\u7684\u5b8c\u6574\u72ec\u7acb\u590d\u6838\u7ed3\u8bba\u3002<\/p>\n

\u8fd9\u91cc\u771f\u6b63\u503c\u5f97\u8ba8\u8bba\u7684\u95ee\u9898\u4e0d\u662fAI\u662f\u5426\u6bd4\u4eba\u66f4\u5feb\uff0c\u4e5f\u4e0d\u662f\u667a\u80fd\u4f53\u80fd\u5426\u53d6\u5f97\u7814\u7a76\u8005\u8eab\u4efd\uff0c\u800c\u662f\uff1a\u5f53\u4e00\u9879AI\u751f\u6210\u7684\u6570\u5b66\u7ed3\u679c\u5df2\u7ecf\u6709\u53ef\u4ee5\u6784\u5efa\u548c\u68c0\u67e5\u7684\u5f62\u5f0f\u8bc1\u660e\u65f6\uff0c\u6211\u4eec\u662f\u5426\u5e94\u5f53\u8bf4\u6570\u5b66\u77e5\u8bc6\u5df2\u7ecf\u786e\u7acb\uff1f<\/p>\n

\u81f3\u5c11\u9700\u8981\u533a\u5206\u56db\u4ef6\u4e8b\u3002\u7b2c\u4e00\uff0c\u7cfb\u7edf\u751f\u6210\u4e86\u4e00\u6bb5\u770b\u4f3c\u5408\u7406\u7684\u6570\u5b66\u6587\u5b57\u3002\u7b2c\u4e8c\uff0cLean\u63a5\u53d7\u4e86\u67d0\u4e2a\u5f62\u5f0f\u9648\u8ff0\u7684\u63a8\u5bfc\u3002\u7b2c\u4e09\uff0c\u8fd9\u4e2a\u5f62\u5f0f\u9648\u8ff0\u51c6\u786e\u8868\u8fbe\u4e86\u4eba\u4eec\u539f\u672c\u8981\u89e3\u51b3\u7684\u6570\u5b66\u95ee\u9898\u3002\u7b2c\u56db\uff0c\u6570\u5b66\u5171\u540c\u4f53\u6709\u5145\u5206\u7406\u7531\u628a\u7ed3\u8bba\u7eb3\u5165\u53ef\u4f9d\u8d56\u3001\u53ef\u89e3\u91ca\u3001\u53ef\u7ee7\u7eed\u4f7f\u7528\u7684\u516c\u5171\u77e5\u8bc6\u3002\u524d\u4e24\u8005\u53ef\u4ee5\u7531\u672c\u6b21\u516c\u5f00\u6750\u6599\u76f4\u63a5\u52a0\u5f3a\uff1b\u540e\u4e24\u8005\u5374\u4e0d\u4f1a\u81ea\u52a8\u968f\u7f16\u8bd1\u6210\u529f\u800c\u5b8c\u6210\u3002<\/p>\n

\u5f62\u5f0f\u9a8c\u8bc1\u7684\u8ba4\u8bc6\u4ef7\u503c\u4e0d\u80fd\u88ab\u4f4e\u4f30\u3002\u4e0e\u53ea\u7ed9\u51fa\u81ea\u7136\u8bed\u8a00\u7b54\u6848\u76f8\u6bd4\uff0c\u8bc1\u660e\u52a9\u624b\u8981\u6c42\u6bcf\u4e00\u6b65\u90fd\u843d\u5728\u660e\u786e\u7684\u5b9a\u4e49\u3001\u7c7b\u578b\u3001\u5b9a\u7406\u548c\u63a8\u7406\u89c4\u5219\u4e2d\u3002OpenAI\u4ed3\u5e93\u8fd8\u7ed9\u51fa\u56fa\u5b9a\u7684Lean\u7248\u672c\u3001\u4f9d\u8d56\u9879\u3001\u6784\u5efa\u6307\u4ee4\u3001\u4e3b\u5b9a\u7406\u4f4d\u7f6e\u3001\u6240\u7528\u516c\u7406\u548c\u72ec\u7acb\u68c0\u67e5\u5de5\u5177\u7684\u5165\u53e3\uff0c\u5e76\u62a5\u544a\u4e3b\u8981\u7ed3\u679c\u6ca1\u6709\u672a\u5b8c\u6210\u7684sorry\u5360\u4f4d\u3002\u8fd9\u4e9b\u6761\u4ef6\u5927\u5e45\u538b\u7f29\u4e86\u542b\u7cca\u8df3\u6b65\u548c\u5c40\u90e8\u903b\u8f91\u9519\u8bef\u53ef\u4ee5\u85cf\u8eab\u7684\u7a7a\u95f4\u3002\u4efb\u4f55\u80fd\u591f\u53d6\u5f97\u4ee3\u7801\u7684\u4eba\uff0c\u539f\u5219\u4e0a\u90fd\u53ef\u4ee5\u91cd\u65b0\u6784\u5efa\uff0c\u5e76\u68c0\u67e5\u5f62\u5f0f\u63a8\u5bfc\u662f\u5426\u88ab\u6307\u5b9a\u7684\u5185\u6838\u63a5\u53d7\u3002\u5c31\u8bc1\u636e\u7ed3\u6784\u800c\u8a00\uff0c\u8fd9\u8fdc\u5f3a\u4e8e\u5f00\u53d1\u8005\u5185\u90e8\u57fa\u51c6\u3001\u8bed\u8a00\u6a21\u578b\u7684\u81ea\u4fe1\u9648\u8ff0\uff0c\u751a\u81f3\u5f3a\u4e8e\u4e00\u7bc7\u53ea\u6709\u81ea\u7136\u8bed\u8a00\u800c\u65e0\u6cd5\u9010\u6b65\u68c0\u67e5\u7684\u957f\u8bc1\u660e\u3002<\/p>\n

\u4f46Lean\u63a5\u53d7\u7684\u662f\u201c\u5728\u8fd9\u4e9b\u5b9a\u4e49\u3001\u8fd9\u4e9b\u516c\u7406\u3001\u8fd9\u4e9b\u5e93\u548c\u8fd9\u4e2a\u5185\u6838\u4e0b\uff0c\u6b64\u5f62\u5f0f\u5b9a\u7406\u53ef\u7531\u524d\u63d0\u63a8\u51fa\u201d\u3002\u5b83\u4e0d\u4f1a\u51ed\u81ea\u8eab\u5224\u65ad\u8be5\u5b9a\u7406\u662f\u5426\u5fe0\u5b9e\u5bf9\u5e94Clay\u95ee\u9898\u4e2d\u7684C\u548cD\uff0c\u4e5f\u4e0d\u4f1a\u81ea\u52a8\u8bc6\u522b\u67d0\u4e2a\u6570\u5b66\u5b9a\u4e49\u867d\u7136\u5728\u5f62\u5f0f\u4e0a\u826f\u597d\uff0c\u5374\u9057\u6f0f\u4e86\u539f\u95ee\u9898\u610f\u56fe\u4e2d\u7684\u6761\u4ef6\u3002\u5f62\u5f0f\u5316\u8005\u5fc5\u987b\u5b8c\u6210\u4ece\u6570\u5b66\u8bed\u5883\u5230\u7b26\u53f7\u5bf9\u8c61\u7684\u7ffb\u8bd1\uff1b\u5185\u6838\u68c0\u67e5\u7ffb\u8bd1\u540e\u7684\u63a8\u5bfc\uff0c\u5374\u4e0d\u80fd\u72ec\u81ea\u4fdd\u8bc1\u7ffb\u8bd1\u524d\u540e\u7684\u95ee\u9898\u76f8\u540c\u3002OpenAI\u4f7f\u7528\u4e86Formal Conjectures\u63d0\u4f9b\u7684\u53c2\u7167\u9648\u8ff0\u6765\u6bd4\u8f83\u8fd9\u79cd\u5bf9\u5e94\uff0c\u8fd9\u662f\u91cd\u8981\u7684\u52a0\u5f3a\uff0c\u4f46\u4ed3\u5e93\u5bf9\u9f50\u8bf4\u660e\u4ecd\u662f\u53d1\u5e03\u65b9\u81ea\u5df1\u7684\u62a5\u544a\uff0c\u9700\u8981\u5916\u90e8\u4e13\u5bb6\u6838\u67e5\u5b9a\u4e49\u3001\u5b9a\u7406\u8303\u56f4\u548c\u53c2\u7167\u4e4b\u95f4\u662f\u5426\u771f\u6b63\u7b49\u4ef7\u3002<\/p>\n

\u6570\u5b66\u77e5\u8bc6\u4e5f\u4e0d\u53ea\u662f\u4e00\u4e2a\u5e03\u5c14\u503c\u5f0f\u7684\u201c\u901a\u8fc7\u201d\u3002\u4e00\u4e2a\u7ed3\u8bba\u8981\u8fdb\u5165\u7814\u7a76\u5171\u540c\u4f53\uff0c\u5176\u4ed6\u4eba\u9700\u8981\u77e5\u9053\u8bc1\u660e\u4f9d\u8d56\u4ec0\u4e48\u3001\u5173\u952e\u6784\u9020\u4e3a\u4f55\u6709\u6548\u3001\u5b83\u4e0e\u5df2\u6709\u7406\u8bba\u600e\u6837\u8854\u63a5\uff0c\u4ee5\u53ca\u5728\u53d7\u5230\u53cd\u4f8b\u3001\u4e0d\u540c\u5f62\u5f0f\u5316\u6216\u7ec6\u8282\u8d28\u7591\u65f6\u80fd\u5426\u88ab\u4fee\u6b63\u3002\u5f62\u5f0f\u8bc1\u4e66\u5c24\u5176\u64c5\u957f\u56de\u7b54\u63a8\u5bfc\u662f\u5426\u5408\u89c4\uff0c\u5374\u672a\u5fc5\u81ea\u52a8\u63d0\u4f9b\u8fd9\u79cd\u89e3\u91ca\u3002166\u9875\u8bc1\u660e\u7a3f\u4e2d\u7684\u7269\u7406\u63cf\u8ff0\u3001\u8bc1\u660e\u7eb2\u8981\u548c\u5b8c\u6574\u4f30\u8ba1\uff0c\u6b63\u662f\u5728\u8fde\u63a5\u5f62\u5f0f\u6b63\u786e\u6027\u4e0e\u6570\u5b66\u7406\u89e3\uff1b\u800c\u4e13\u5bb6\u9605\u8bfb\u3001\u72ec\u7acb\u91cd\u5efa\u548c\u66ff\u4ee3\u68c0\u67e5\uff0c\u5219\u662f\u5728\u68c0\u9a8c\u8fd9\u6761\u8fde\u63a5\u662f\u5426\u7262\u56fa\u3002<\/p>\n

\u8fd9\u4e0d\u662f\u628a\u771f\u7406\u4ea4\u7ed9\u591a\u6570\u6295\u7968\u3002\u82e5\u4e00\u4e2a\u6b63\u786e\u5f62\u5f0f\u5316\u7684\u5b9a\u7406\u5df2\u7ecf\u7531\u53ef\u9760\u5185\u6838\u63a8\u5bfc\u51fa\u6765\uff0c\u5171\u540c\u4f53\u4e0d\u80fd\u9760\u4e0d\u559c\u6b22\u5b83\u800c\u4f7f\u5b83\u4e3a\u5047\u3002\u95ee\u9898\u5728\u4e8e\uff0c\u6211\u4eec\u5f53\u524d\u8981\u5224\u65ad\u7684\u5bf9\u8c61\u4e0d\u662f\u62bd\u8c61\u7684\u63a8\u5bfc\u4e32\uff0c\u800c\u662f\u201c\u8fd9\u4e2a\u4ed3\u5e93\u8bc1\u660e\u4e86Clay\u6240\u95ee\u7684Navier\u2013Stokes\u547d\u9898\u201d\u8fd9\u4e00\u590d\u5408\u4e3b\u5f20\u3002\u590d\u5408\u4e3b\u5f20\u5305\u542b\u5b9a\u7406\u8868\u8ff0\u3001\u8bed\u4e49\u5bf9\u5e94\u3001\u8f6f\u4ef6\u4fe1\u4efb\u3001\u4f9d\u8d56\u7ba1\u7406\u548c\u6570\u5b66\u89e3\u91ca\u3002\u5b83\u4eec\u4e2d\u7684\u4efb\u4f55\u4e00\u9879\u51fa\u73b0\u9519\u4f4d\uff0c\u90fd\u53ef\u80fd\u4f7f\u201c\u5f62\u5f0f\u8bc1\u660e\u6709\u6548\u201d\u548c\u201c\u539f\u95ee\u9898\u5df2\u89e3\u51b3\u201d\u540c\u65f6\u4e00\u771f\u4e00\u5047\u3002<\/p>\n

\u4ece\u7ef4\u6210\u8bba\u770b\uff0cDifference\u9996\u5148\u8981\u6c42\u628a\u81ea\u7136\u8bed\u8a00\u8bba\u6587\u3001Lean\u5b9a\u7406\u3001Clay\u539f\u95ee\u9898\u548c\u516c\u5171\u77e5\u8bc6\u4e3b\u5f20\u533a\u5206\u5f00\u6765\uff1b\u8fd9\u4e9b\u4e0d\u662f\u540c\u4e00\u5bf9\u8c61\u7684\u56db\u79cd\u540d\u79f0\u3002Constraint\u4e0d\u662f\u6cdb\u6307\u9650\u5236\uff0c\u800c\u662f\u5b9a\u4e49\u3001\u516c\u7406\u3001\u7c7b\u578b\u7cfb\u7edf\u3001\u5e93\u7248\u672c\u3001\u5185\u6838\u3001\u6784\u5efa\u73af\u5883\u548c\u540c\u884c\u8d28\u7591\u5171\u540c\u6784\u6210\u7684\u5f62\u6210\u6761\u4ef6\uff1a\u5b83\u4eec\u4f7f\u67d0\u4e9b\u63a8\u5bfc\u53ef\u4ee5\u6210\u7acb\uff0c\u4e5f\u6392\u9664\u53e6\u4e00\u4e9b\u63a8\u5bfc\u3002Sustained Coherence\u5219\u8981\u6c42\u5f62\u5f0f\u9648\u8ff0\u3001\u975e\u5f62\u5f0f\u8bc1\u660e\u3001\u539f\u59cb\u95ee\u9898\u548c\u72ec\u7acb\u590d\u6838\u4e4b\u95f4\u7684\u5bf9\u5e94\uff0c\u5728\u91cd\u590d\u6784\u5efa\u3001\u4e13\u5bb6\u5ba1\u67e5\u3001\u53cd\u4f8b\u641c\u7d22\u548c\u7248\u672c\u4fee\u6b63\u4e2d\u6301\u7eed\u4fdd\u6301\u4e00\u81f4\u3002\u8fd9\u91cc\u7684\u201c\u6301\u7eed\u201d\u5f88\u91cd\u8981\uff0c\u56e0\u4e3a\u4e00\u6b21\u6210\u529f\u6784\u5efa\u53ea\u80fd\u8bc1\u660e\u67d0\u4e2a\u56fa\u5b9a\u72b6\u6001\u4e0b\u7684\u5f62\u5f0f\u5173\u7cfb\uff0c\u4e0d\u80fd\u66ff\u4ee3\u8de8\u5de5\u5177\u3001\u8de8\u89e3\u91ca\u548c\u8de8\u5ba1\u67e5\u8005\u7684\u6821\u6b63\u3002<\/p>\n

\u6211\u7684\u5224\u65ad\u662f\uff0c\u8fd9\u6b21\u516c\u5f00\u6750\u6599\u5df2\u7ecf\u5efa\u7acb\u4e86\u4e00\u4e2a\u5f3a\u5ea6\u5f88\u9ad8\u3001\u53ef\u516c\u5f00\u68c0\u9a8c\u7684\u6570\u5b66\u77e5\u8bc6\u5019\u9009\u3002\u82e5\u4ed3\u5e93\u80fd\u7531\u72ec\u7acb\u56e2\u961f\u91cd\u5efa\uff0c\u5f62\u5f0f\u9648\u8ff0\u4e0eClay\u539f\u547d\u9898\u7684\u5bf9\u5e94\u5f97\u5230\u4e13\u5bb6\u786e\u8ba4\uff0c\u8bc1\u660e\u7a3f\u7684\u5173\u952e\u6784\u9020\u548c\u4f30\u8ba1\u4e5f\u7ecf\u5f97\u8d77\u5ba1\u67e5\uff0c\u90a3\u4e48\u5f62\u5f0f\u9a8c\u8bc1\u5b8c\u5168\u53ef\u4ee5\u6210\u4e3a\u6570\u5b66\u77e5\u8bc6\u786e\u7acb\u7684\u6838\u5fc3\u90e8\u5206\uff0c\u800c\u4e0d\u53ea\u662f\u8f85\u52a9\u8bc1\u636e\u3002\u4f46\u5728\u5f53\u524d\u9636\u6bb5\uff0c\u6700\u51c6\u786e\u7684\u8bf4\u6cd5\u4ecd\u662f\uff1aOpenAI\u516c\u5f00\u4e86\u4e00\u9879\u5e26\u6709\u673a\u5668\u53ef\u68c0\u9a8c\u8bc1\u4e66\u7684\u89e3\u51b3\u4e3b\u5f20\uff1b\u5f62\u5f0f\u7cfb\u7edf\u5185\u7684\u63a8\u5bfc\u83b7\u5f97\u4e86\u5f00\u53d1\u8005\u81ea\u8bc4\u652f\u6301\uff0c\u516c\u5171\u6570\u5b66\u77e5\u8bc6\u7684\u5b8c\u6574\u786e\u8ba4\u8fc7\u7a0b\u5c1a\u672a\u5b8c\u6210\u3002<\/p>\n

\u8fd9\u4e2a\u5224\u65ad\u4e0d\u8981\u6c42\u6bcf\u4f4d\u6570\u5b66\u5bb6\u4eb2\u81ea\u8bfb\u5b8c\u6bcf\u4e00\u884c\u4ee3\u7801\uff0c\u4e5f\u4e0d\u9884\u8bbeAI\u4e0d\u80fd\u4ea7\u751f\u771f\u6b63\u7684\u65b0\u6570\u5b66\u3002\u5b83\u53ea\u9650\u5b9a\u6211\u4eec\u4eca\u5929\u53ef\u4ee5\u4ece\u73b0\u6709\u8bc1\u636e\u63a8\u51fa\u4ec0\u4e48\u3002\u672a\u6765\u6700\u6709\u8fa8\u522b\u529b\u7684\u8bc1\u636e\u4e0d\u662f\u66f4\u591a\u6a21\u578b\u81ea\u8ff0\u6216\u66f4\u5927\u7684\u667a\u80fd\u4f53\u6570\u91cf\uff0c\u800c\u662f\u72ec\u7acb\u6784\u5efa\u8bb0\u5f55\u3001\u5f62\u5f0f\u9648\u8ff0\u7684\u8bed\u4e49\u5ba1\u8ba1\u3001\u4e13\u5bb6\u5bf9\u5173\u952e\u6784\u9020\u7684\u590d\u6838\u3001\u53ef\u56de\u7b54\u7684\u5177\u4f53\u5f02\u8bae\uff0c\u4ee5\u53ca\u53d1\u73b0\u9519\u4f4d\u540e\u53ef\u8ffd\u8e2a\u7684\u4fee\u8ba2\u3002<\/p>\n

\u53c2\u8003\u8d44\u6599<\/p>\n

https:\/\/openai.com\/index\/navier-stokes-solution\/<\/a><\/p>\n

\u70b9\u51fb\u4ee5\u8bbf\u95ee navier-stokes.pdf<\/a><\/p>\n<\/p>\n

https:\/\/github.com\/openai\/NavierStokesAndEuler<\/a><\/p>\n

https:\/\/www.theguardian.com\/science\/2026\/sep\/08\/openai-claims-to-have-solved-maths-problem-that-stumped-humans-for-decades<\/a><\/p>\n

\u70b9\u51fb\u4ee5\u8bbf\u95ee navierstokes.pdf<\/a><\/p>\n<\/p>\n

https:\/\/plato.stanford.edu\/archives\/sum2026\/entries\/mathematical-practice\/<\/a><\/p>\n

","protected":false},"excerpt":{"rendered":"","protected":false},"author":17897162,"featured_media":0,"comment_status":"","ping_status":"","sticky":false,"template":"","format":"standard","meta":{"_coblocks_attr":"","_coblocks_dimensions":"","_coblocks_responsive_height":"","_coblocks_accordion_ie_support":"","_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":true,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"_geoff_meta_description_en":"Using OpenAI\u2019s Navier\u2013Stokes manuscript and Lean formalisation, this essay distinguishes formal derivation, faithful statement encoding, mathematical understanding and public knowledge, arguing that machine verification is strong evidence but not yet the whole epistemic case.","_geoff_meta_description_zh":"\u4ee5OpenAI\u516c\u5f00\u7684Navier\u2013Stokes\u8bc1\u660e\u7a3f\u548cLean\u5f62\u5f0f\u5316\u4e3a\u8d77\u70b9\uff0c\u533a\u5206\u5f62\u5f0f\u7cfb\u7edf\u5185\u63a8\u5bfc\u3001\u547d\u9898\u5bf9\u5e94\u3001\u6570\u5b66\u7406\u89e3\u4e0e\u516c\u5171\u77e5\u8bc6\uff0c\u8bf4\u660e\u673a\u5668\u9a8c\u8bc1\u4e3a\u4f55\u662f\u5f3a\u8bc1\u636e\u4f46\u4e0d\u662f\u5f53\u524d\u9636\u6bb5\u7684\u5168\u90e8\u8ba4\u8bc6\u6761\u4ef6\u3002","_wpcom_ai_launchpad_first_post":false,"_jetpack_feature_clip_id":0,"_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","default_image_id":0,"font":"","enabled":false},"version":2},"jetpack_post_was_ever_published":false},"categories":[787298291],"tags":[787298294,787294346,787294331,787298292,787294332,787294292,787298293,787298295],"class_list":["post-19670","post","type-post","status-publish","format-standard","hentry","category-ai-philosophy-observation","tag-ai-and-humanity","tag-artificial-intelligence","tag-787294331","tag-philosophy-of-ai","tag-sustenesis-theory","tag-787294292","tag-philosophy-of-ai-zh","tag-ai-and-humanity-zh",""],"translatepress_titles":{"en_AU":"AI Philosophy Observations | Formal Verification Is Not Yet Mathematical Knowledge","zh_CN":"AI\u54f2\u5b66\u89c2\u5bdf\uff5c\u5f62\u5f0f\u9a8c\u8bc1\u901a\u8fc7\u4e0d\u7b49\u4e8e\u6570\u5b66\u77e5\u8bc6\u5df2\u7ecf\u786e\u7acb"},"jetpack_publicize_connections":[],"jetpack_likes_enabled":false,"jetpack_sharing_enabled":true,"jetpack_shortlink":"https:\/\/wp.me\/p1ar9H-57g","jetpack_featured_media_url":"","_links":{"self":[{"href":"https:\/\/geoffreychen.com\/zh\/wp-json\/wp\/v2\/posts\/19670","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/geoffreychen.com\/zh\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/geoffreychen.com\/zh\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/geoffreychen.com\/zh\/wp-json\/wp\/v2\/users\/17897162"}],"replies":[{"embeddable":true,"href":"https:\/\/geoffreychen.com\/zh\/wp-json\/wp\/v2\/comments?post=19670"}],"version-history":[{"count":0,"href":"https:\/\/geoffreychen.com\/zh\/wp-json\/wp\/v2\/posts\/19670\/revisions"}],"wp:attachment":[{"href":"https:\/\/geoffreychen.com\/zh\/wp-json\/wp\/v2\/media?parent=19670"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/geoffreychen.com\/zh\/wp-json\/wp\/v2\/categories?post=19670"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/geoffreychen.com\/zh\/wp-json\/wp\/v2\/tags?post=19670"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}