Logic Theorist 完成定理证明

38 比 52。

艾伦·纽厄尔、赫伯特·西蒙和克利夫·肖的 Logic Theorist，在怀特海与罗素《数学原理》第二章选取的 52 个命题中证明了 38 个；其中一项证明比原书更短。命题本身早已成立，印刷页上甚至附有证明。程序要做的不是发现终点，而是在许多合法步骤之间选出一条能抵达终点的路。

形式逻辑规定什么可以做，却不自动规定先试哪一步。若把所有分支一视同仁，候选路径会迅速增殖。团队把证明表示为状态空间搜索：当前有哪些已知表达式，哪些推理规则可以施用，下一步可能生成什么。所谓启发式，就是给这些可能性排出先后，尽早放弃看起来无望的方向。RAND 公司对这台“逻辑理论机器”的说明特意把它与通常的系统算法区分开来：它倚重与人类解题活动相似的启发方法——“相似”不是说机器具有数学家的直觉生活，而是说程序开始处理一种此前常被藏在结果之外的工作：选择。纽厄尔与西蒙后来把这类方法概括为有限理性在计算中的对应物：在资源有限时，不求穷尽全部合法路径，而求尽快找到足够好的一条。

未能证明的 14 个命题同样属于成绩单。它们标出了当时搜索深度、启发式偏好与机器资源的交界，而不是“机器不会数学”的笼统结论。较短的那条证明之所以有价值，正因为旁人可以逐步核对它是否每一步都合乎规则——机器没有神秘权威，只有可审计的路径。

为了让搜索能在 1950 年代的机器上运行，团队还得解决一个不那么哲学的问题：程序怎样保存长度不断变化的符号表达式、证明目标和候选步骤。纽厄尔、肖与西蒙为此开发了信息处理语言 IPL，以链表组织符号结构，使列表可以动态增删、嵌套与共享。今天看来，数据结构像实现细节；在当时，它却是“让机器操作观念”不可分割的一半。没有能增删、重排和共享符号片段的表示，启发式策略无处落脚。Logic Theorist 也因此与数值计算程序分道：算术程序处理固定格式的数字；它处理可重写的表达式树。

早期电子计算机最容易被理解为高速算术设备。Logic Theorist 让符号本身成为机器操作的对象，让中间状态、目标差距和策略偏好进入程序。“该试什么”开始与“怎么算”同样重要。1956 年达特茅斯暑期研究项目召开时，纽厄尔与西蒙已经能展示这套系统的部分成果；符号 AI 随后数十年的主流议程——表示、搜索、启发式——在这里有了一份可演示的样板。

纽厄尔与西蒙后来把这种思想推向更一般的问题求解，包括 GPS 等后续系统。Logic Theorist 本身仍适合留在它实际完成的尺度上：一个边界清楚的形式系统、一批已知命题、一套经过设计的选择规则，以及 38/52 这一可以逐行核对的成绩单。后来的符号系统换了领域，仍常重复同一骨架：先表示状态，再在合法算子中搜索，并用启发式控制爆炸。贡献不在“会做全部数学”，而在把这一骨架做成了可运行的第一件样品。

38 out of 52.

Allen Newell, Herbert Simon, and Cliff Shaw’s Logic Theorist proved 38 of 52 selected propositions from chapter two of Whitehead and Russell’s Principia Mathematica. One proof was shorter than the published version. The propositions were already known to be true; printed proofs were already attached. The program’s problem was not to discover the destination but to find a route to it.

Formal logic says which steps are allowed. It does not automatically say which permitted step should be tried first. Treat every branch equally and candidate paths grow beyond practical reach. The team represented proof as a search through states—known expressions, applicable rules, possible next formulas—and supplied heuristics for ranking those possibilities. Preference under resource limits, not exhaustive enumeration, became part of the program. RAND’s description of the “logic theory machine” emphasized the difference from a systematic algorithm that mechanically exhausts its options: its methods were called heuristic because they resembled a limited but central feature of human problem solving—selection when the search space is too large to finish. The resemblance did not grant the machine a mathematician’s private intuition. It meant that the labor often omitted when a clean proof is printed—deciding what to try next—had become procedural. Newell and Simon would later connect this style of work to bounded rationality: a system that cannot survey every lawful path must still choose well enough, soon enough.

The 14 failures belong on the same scorecard. They mark the joint limits of search depth, heuristic preference, and machine resources—not a general verdict that machines cannot do mathematics. The shorter proof mattered because another reader could verify, line by line, whether each inference obeyed the rules. The program held no occult authority—only an auditable path.

Making that search run on a 1950s computer required an unglamorous companion invention. Newell, Shaw, and Simon developed the Information Processing Language, or IPL, to hold symbolic expressions, goals, and candidate steps in linked lists whose length could change. Lists could grow, nest, and share structure. A data structure can look like plumbing in retrospect. Here it was part of the intellectual claim. Heuristics could not choose among ideas until the machine had a practical way to construct, rearrange, and share their symbolic pieces. Logic Theorist therefore diverged from numerical programs: arithmetic code handled fixed-format numbers; this program rewrote expression trees.

Early electronic computers were easy to understand as fast arithmetic machinery. Logic Theorist worked on symbolic expressions, intermediate states, goals, and estimates of promise. Calculation now included deciding what deserved calculation next. By the time of the 1956 Dartmouth summer project, Newell and Simon could already exhibit results from this line of work. The later mainstream of symbolic AI—representation, search, heuristics—had a demonstrable prototype at a scale small enough to check line by line.

Newell and Simon would pursue a more general science of problem solving, including later systems such as GPS. Logic Theorist itself remains clearest at its actual scale: one formal system, a selected collection of propositions, designed rules of preference, and a score of 38 out of 52 that can still be audited. Later symbolic systems changed domains while repeating the same skeleton: represent states, search among legal operators, control explosion with heuristics. The contribution was not that it “did all of mathematics,” but that it made the skeleton run as a first working sample.