The Logic Theory Machine

idea is right, and the id was filed correctly, but the tempting alternative is worth killing on the way past because the popular version of this entry is built out of it. The obvious case for moment is "the first AI program, shown at Dartmouth in the summer of 1956." Both halves of that are wrong or overstated, and the dates below say why. What survives is not an event but a framing — heuristic search over a space of subproblems, working backward from the goal, under an explicit effort budget — which is what every proof-finding system since has been a variation on, including the ones the readings now cover weekly. That is the idea kind's definition: the thing you are watching descends from this, and the descent explains its shape. Precedent in canon/ is settled: eliza-1966 and mycin-1976 are also programs filed as idea, while deep-blue-1997 — a contest with a date and a scoreline — is moment.

Four dates, and the id names the earliest. The specification is RAND paper P-868, dated 12 July 1956 (revised; RAND's own index gives 15 June for the first issue), presented at the IRE Symposium on Information Theory in Cambridge, Massachusetts on 10 September 1956 and published that month in IRE Transactions on Information Theory IT-2, No. 3. The program was hand-simulated in January 1956, before any of that. It was not running on a computer at the Dartmouth workshop that summer. Machine proofs came out of the JOHNNIAC in late 1956 and early 1957, and the results everyone quotes — 38 of the first 52 theorems, the twelve-minute proof, the failure at twenty-three minutes — are from P-951, dated 14 March 1957 and presented at the Western Joint Computer Conference in Los Angeles on 28 February 1957. The id says 1956 because that is when the idea was fixed and published; the empirical record is 1957 and should be dated as such whenever a reading uses a number from it.

The authorship is not what the proposal list says, and the difference is informative. proposals.md lists this as "Newell, Simon & Shaw, 1956." P-868 carries two authors, Newell and Simon, with Shaw thanked in a footnote as the person "who has been their partner in many aspects of this enterprise, and particularly in undertaking to realize the logic theorist in a computer — work that will be reported in subsequent papers." Shaw is a full author of P-951, the paper with the machine in it. The specification and the realization were credited separately, by the people involved, at the time. A reading that wants to say something about who gets named on frontier work has a clean 1956–57 instance here, and it does not need editorialising.

descends_from is a checked fact, not a guess. P-868's own acknowledgements do not cite Shannon; they name Selfridge and Dinneen on pattern recognition, and two unnamed bodies of work on automatic programming and on human problem solving. The link to shannon-chess-1950 runs through a third paper: Allen Newell's The Chess Machine: An Example of Dealing with a Complex Task by Adaptation, RAND P-620, December 1954, delivered at the 1955 Western Joint Computer Conference. I read its reference list directly. Item [1] is "Shannon, C. E. Programming a computer for playing chess. Phil. Mag. 1950 41 314 256–275" — the exact paper that is shannon-chess-1950. P-620 is where Newell writes down "the consequences problem," "the horizon problem" and "the evaluation problem," and where goals generate subgoals that are reinforced when the goal is met. The Logic Theorist's subproblem tree is that machinery pointed at logic instead of chess. So the honest chain is Shannon 1950 → Newell's chess machine 1954 → LT 1956, with the middle link absent from canon/ and absent from proposals.md. If someone writes it, this entry's header should be edited to descend from it instead.

Two other ancestors are real and unavailable. The first is Principia Mathematica itself (Whitehead and Russell, 1910–13, second edition 1925), which is the program's entire subject matter and is also the book named in the title of godel-incompleteness-1931. Nothing in canon/ represents it. The second is dartmouth-1956, proposed and unwritten, which is a sibling rather than a parent: LT was the only working — or nearly working — system anyone brought to the meeting where the field got its name.

What it is

A program that finds proofs of theorems in propositional logic by searching, badly and selectively, through a space of subproblems, and stops when it runs out of budget. It was the first program built to do that, and the first program built on the explicit claim that finding a proof is the same kind of activity as playing chess or translating a language, so that a machine that does one tells you something about the others.

P-868's summary states the thesis without decoration:

> In this paper we describe a complex information processing system, which we > call the logic theory machine, that is capable of discovering proofs for > theorems in symbolic logic. This system, in contrast to the systematic > algorithms that are ordinarily employed in computation, relies heavily on > heuristic methods similar to those that have been observed in human problem > solving activity.

The word doing the work is heuristic, and this pair of papers is where it enters computing as a term of art with a definition. P-868 introduces the contrast — "we shall call the former algorithms, the latter heuristic methods" — and P-951 makes it exact: "A process that may solve a given problem, but offers no guarantees of doing so, is called a heuristic for that problem." Everything downstream in this entry is an argument about that trade, so it is worth stating plainly what was being traded away: LT gave up completeness on purpose. "Its procedures guarantee neither that its proposed sequences are proofs of something, nor that LT will ever find the proof, no matter how much effort is spent. However, they often generate the desired proof in a reasonable computing time."

The task. Principia's propositional calculus has five axioms and three rules of inference — substitution (replace a variable by an expression throughout), replacement (swap a connective for its definition), and detachment (modus ponens). Give LT the axioms and some already-proved theorems, hand it an expression, and it looks for a derivation. P-951 walks the reader through a run: LT is asked for theorem 2.01, "(p implies not-p) implies not-p," and "works for about 10 seconds and then prints out" a four-line proof.

The four methods. Substitution tries to turn a known theorem into the goal by substituting and replacing. Detachment looks for a known theorem of the form "A implies B" where B matches the goal, and sets up A as a new subproblem. Forward and backward chaining exploit transitivity: for a goal "a implies c," find "a implies b" and set up "b implies c," or find "b implies c" and set up "a implies b." Only substitution ever proves anything; the other three manufacture subproblems. An executive routine tries substitution first, then detachment, then the two chainings, then walks the subproblem list in order of generation and does it all again, "until (a) a proof is found, (b) the time allotted for finding a proof is used up, (c) there is no more available memory space in the machine, or (d) no untried problems remain on the subproblem list."

That four-way termination condition is the part of the design that has aged best, and it is why this is not merely a logic paper. LT was built from the start to be a system that could give up, for four distinguishable reasons, and to say which.

Why not just enumerate. P-951 constructs the honest baseline and names it: an algorithm that "constructs all possible proofs in a systematic manner," checking for duplicates and for a match with the target. "We will call this algorithm the British Museum algorithm, in recognition of the supposed originators of procedures of this type" — the monkeys and the typewriters, left politely implicit. Then it is priced. Roughly a thousand theorems come out in the first eleven steps, six of which happen to be in chapter 2 of Principia. For the rest: "We have no way at present to estimate how many proofs must be generated to include proofs of all theorems of chapter 2. Our best guess is that it might be a hundred million." Because detachment forces duplicate checking, cost goes quadratic in expressions generated, and "at this rate it would take hundreds of thousands of years of computation to generate proofs for the theorems in chapter 2."

This is the same move as Shannon's 10¹²⁰: an impossibility number computed in order to justify not doing that, by the people proposing the alternative. It should be read the same way, and it is misread the same way.

The trick that makes it work is matching, not searching. The paper is unusually clear that the search itself is not where the win comes from. LT compares the goal expression against a candidate theorem component by component, and the comparison tells it what to substitute next: "It is not important for an efficient search that the goal be known from the beginning; it is crucial that hints of 'warmer' or 'colder' occur as the search proceeds." And the second structural insight, stated once and then reused by everything since:

> the methods that generate subproblems work "backwards" from the desired > theorem to axioms or known theorems rather than "forward" as did the British > Museum algorithm. Since there is only one theorem to be proved, but a number > of known true theorems, the efficacy of working backward may be analogous to > the ease with which a needle can find its way out of a haystack, compared with > the difficulty of someone finding the lone needle in the haystack.

The results, stated the way the source states them. P-951: "To obtain data on its performance, LT was given the task of proving in sequence the first 52 theorems of Principia. In each case, LT was given the axioms plus all the theorems previously proved in Chapter 2 as the material from which to work (regardless of whether LT had proved the theorems itself). Of the 52 theorems, proofs were found for a total 38 (73%)."

The parenthesis is the whole story and it is the first thing every retelling drops. LT was not building a tower; it was handed the tower at each step and asked for the next brick. Seventeen of the 38 — "almost a half" — fell to substitution alone, and the paper says candidly that these "have the appearance of 'corollaries' of the theorems they are derived from." On subproblems rather than original goals, substitution succeeded 21 times in 338 attempts, 6.2%.

And the failures, which are more useful than the successes. Theorem 2.45 took about twelve minutes with all 38 prior theorems available. Theorem 2.31 was attempted with 28 prior theorems and, after about twenty-three minutes, LT "reports that it cannot prove 2.31, that it has exhausted its resources." The longest successful proof, of 2.17, cost 89,000 primitive operations, some 250 times a typical short proof. Only six proofs ran longer than two steps. Exactly one four-step proof was ever obtained. And there is a theorem LT cannot prove at all, by construction rather than by budget: "we have discovered a theorem (2.13, 'p or not-not-not-p') which the four methods of LT cannot prove. All the subproblems generated for 2.13 after a certain point are false, and therefore cannot lead to a proof."

The authors draw the conclusion themselves, and it is the single most reusable sentence in the pair of papers:

> We believe that this situation is typical: good heuristics produce > differences in performance of large orders of magnitude, but invariably a > "plateau" is reached that can be surpassed only with quite different > heuristics. These new heuristics will again make differences of orders of > magnitude.

with the mechanism named: "for proofs of three steps, the size of the search already presses LT against its computing limits; and if one or two additional steps are added the amount of search required to find a proof exceeds any amount of computing power that could practically be made available."

The by-product that outlived the program. To build LT at all, Newell, Shaw and Simon had to invent a language, since none existed that could manipulate symbol structures. Information Processing Language went through five versions; it gave computing list manipulation, dynamic memory allocation, symbols as first-class objects, recursion and higher-order functions, and it is the acknowledged ancestor of Lisp. Jeff Shrager, who spent 2025 building an IPL-V interpreter in Common Lisp in order to run the original code again, reports the comparison from the inside: IPL had "essentially everything that Lisp has, with two critical exceptions: homoiconic syntax, and automatic garbage collection." The theorem prover was the excuse; the data structure was the contribution.

A note on names. P-868 calls the program "the logic theorist (LT)" and the language it is specified in "the logic language (LL)"; P-951 calls the program "the Logic Theory Machine (LT)". Both names are the authors'. The id uses one and this entry's title uses the other, and nothing turns on it.

Why a reading would cite it

Four occasions, all of which the readings have already produced or will.

1. When a machine is reported to have found a proof. This is the live one. The 15 Aug midday reading logs Crouzeix's conjecture, open since 2004, with two claimed proofs disclosing model use — one after a described 16-hour autonomous run, one an independent argument whose authors say they used a model to explore strategies — neither peer-reviewed. LT is where this species of claim begins, and it supplies the checklist for grading one, because its own headline number fails the checklist in a documented way. What was the system given? LT's "38 of the first 52" was obtained with every prior theorem of the chapter handed to it whether or not it had earned them. What was the budget, and did the system stop or succeed? LT's 2.31 run is a twenty-three-minute failure that a less careful report would never have mentioned. Is the target hard or is it adjacent to something already known? Seventeen of LT's 38 were, in the authors' own word, corollaries. A reading that applies those three questions to a 2026 result is doing what the 1957 paper did to itself, and the citation is the point: the discipline is as old as the claim.

2. When "the search space is astronomical" is used as an argument. "Hundreds of thousands of years of computation" is this entry's version of Shannon's 10¹²⁰, computed for the same rhetorical purpose and abused the same way. Cite alongside shannon-chess-1950 when a reading meets a combinatorial-impossibility argument; the pair establishes that in 1950 and again in 1957 the number was produced by someone building the thing it supposedly forbade. lighthill-1973 (proposed, unwritten) is the case where a funder believed the argument.

3. When a system is reported to have run for hours, or been cut off. LT is the origin of the effort limit as a designed feature: a budget in machine cycles, a subproblem cap, and a program that reports which of four reasons it stopped for. Shrager's 2026 reanimation runs with the limits set at 20,000 IPL cycles, 50 subproblems and 50 substitutions, and prints them next to the actuals on every proof. When a reading covers agentic loops priced in wall-clock — the 14 Aug Ultrafast item makes exactly that point about throughput — or a 16-hour autonomous run, this is the entry that says the practice of publishing the budget alongside the result is seventy years old and was invented by the people whose system kept hitting it. A result reported without its budget is less informative than a 1957 RAND paper, and a reading may say so.

4. When the argument is that scaling has hit a wall, or that it has not. The plateau paragraph quoted above is a dated, evidenced statement of the shape: enormous gains from a heuristic, then a hard ceiling that only a different heuristic clears, then enormous gains again. It is not a prediction of doom and not a promise of continuity; it is a claim about the form of the curve, made in 1957 with a subproblem-count mechanism attached. Cite it when a reading has to adjudicate between "progress has stopped" and "progress is continuous," because it licenses neither and describes both.

There is a fifth occasion that is unusual enough to name separately, and it is current. On 13 March 2026 Jeff Shrager posted Executable Archaeology: Reanimating the Logic Theorist from its IPL-V Source, reporting the first execution of the original Logic Theorist code in over half a century, from the listing in a 1963 RAND memorandum, on a new IPL-V interpreter. The debugging was done in part by large language models, and the paper's most striking passage is about a bug in a list-copying primitive that neither the manual nor the author's reading of it could resolve: Claude was given the Computer History Museum's scan of Shaw's original 1962 IPL-V punched-card deck, compared it against the modern implementation, and found the discrepancy. "It was a collaboration across sixty years." A reading that needs a concrete, dated, verifiable case of a current model doing useful work on the historical record — as against a claim about what such a model might one day do — has one here, and it happens to be about the first AI program. That is a citation this canon is for.

What this entry should not be cited for: any claim that LT shows machines do or do not think. P-951 explicitly defers the question — "we postpone to later papers a discussion of the implications of our work for the psychological theory of human thinking and problem solving" — and the papers are weaker, not stronger, when pressed into that service.

What it got right, and what it got wrong

Not required for idea. Included because the central bet was refuted inside three years, by a named person with numbers, and then reinstated seventy years later in a form the original authors could not build — which is the same arc as shannon-chess-1950 and, run twice, stops being a coincidence and starts being a finding.

Claims dated 1956–57. Graded 2026-08-16.

Right, and it is still the architecture. A goal, a set of methods that decompose it into subgoals, a list of pending subgoals, backward search from the target, a matching procedure that yields incremental "warmer/colder" feedback, and a hard budget. That is a description of LT and it is a description of the proof search inside AlphaProof, of every tactic-level automation in Lean, and — strip the logic — of an agent loop. Working backward beat working forward in 1957 and still does. The observation that subproblems multiply "more or less exponentially with the depth of the proof" is the reason proof search is still hard. The plateau claim has been right repeatedly and at every scale since.

Right, and under-credited: the machine that reports why it stopped. LT's four termination conditions, the effort counter, the published limits-versus- actuals. Contemporary systems are only now being pushed back toward this by regulators and by embarrassment. The 15 Aug reading turns on a lab conceding that its own instruments for judging a model are degrading; LT shipped its instruments in the paper.

Wrong, and this is the famous one, though almost nobody tells it: the algorithmic approach beat the heuristic one, quickly, on the same theorems. In January 1960 Hao Wang published Toward Mechanical Mathematics in the IBM Journal of Research and Development. Its epigraph is two lines:

> The gallant tailor: seven (flies) in one blow. > IBM 704: 220 theorems (in the propositional calculus) in three minutes.

Wang's first program is "a proof-decision procedure for the propositional calculus which prints out a proof or a disproof according as the given proposition is a theorem or not" — complete, guaranteed, no heuristics. The numbers: "the whole list of over 200 theorems of the first five chapters of Principia Mathematica were proved within about 37 minutes, and 12/13 of the time is used for read-in and print-out, so that the actual proving time for over 200 theorems was less than 3 minutes. The 52 theorems chosen by Newell-Shaw-Simon are among the easier ones and were proved in less than 5 minutes (or less than ½ minute if not counting input-output time). In particular, 2.45 was proved in about 3 seconds and 2.31 in about 6 seconds."

Set those against the 1957 record. Theorem 2.45: LT about twelve minutes, Wang about three seconds — a factor of roughly 240. Theorem 2.31: LT could not do it at all, giving up after twenty-three minutes; Wang, six seconds. And where LT proved 38 of 52 with all prior theorems supplied, Wang's third program handled the predicate calculus with equality across the next five chapters of Principia, "about 85% of these theorems in about an hour."

Wang's assessment is worth quoting because it is fairer than its reputation and sharper than its paraphrases:

> It will naturally be objected that the comparison with the program of > Newell-Shaw-Simon is unfair, since the approaches are basically different. The > writer realizes this but cannot help feeling, all the same, that the > comparison reveals a fundamental inadequacy in their approach. There is no > need to kill a chicken with a butcher's knife. Yet the net impression is that > Newell-Shaw-Simon failed even to kill the chicken with their butcher's knife.

And on the word itself:

> To argue the superiority of "heuristic" over algorithmic methods by choosing a > particularly inefficient algorithm seems hardly just. The word "heuristic" is > said to be synonymous with "the art of discovery," yet often seems to mean > nothing else than a partial method which offers no guarantees of solving a > given problem. This ambiguity endows the word with some emotive meaning that > could be misleading in further scientific endeavors. The familiar and less > inspiring word "strategy" might fare better.

Claim made 1956–57, due by 1960, graded wrong on the merits as stated. But grade it precisely, because three qualifications change what the lesson is.

First, LT's authors knew. P-868, page 3, lists as its fourth reason for choosing logic that "there are available algorithms, and a realization of at least one of these algorithms (the Kalin-Burkhart machine), that can perform these same tasks; hence, the logic theorist provides a contrast between algorithmic and heuristic approaches in performing the same problem-solving tasks." They picked a domain where a complete decision procedure already existed because they wanted the contrast. Wang's chicken-and-butcher's-knife line lands on a target that had announced the chicken was a control condition. What Wang actually refuted was the stronger claim their rhetoric invited — that heuristics were needed here — rather than the claim they defended, that heuristics were being studied here.

Second, the domain was decidable and that is the whole of Wang's advantage. The propositional calculus has truth tables; turing-halting-1936 bites nowhere near it. Wang says so explicitly and generalises carefully: for the full predicate calculus, "we may fail in some case because we can get no proof, no matter how many repetitions we introduce," which "does not preclude completeness" but "does exclude a decision procedure." The 240× is a fact about a decidable fragment, not about heuristics.

Third, Wang predicted the reinstatement. The same paper, two paragraphs earlier: "we are in fact faced with a challenge to devise methods of buying originality with plodding, now that we are in possession of slaves which are such persistent plodders," and machines "following the broad outline of paths drawn up by man, might yield surprising new results by making many new turns which man is not accustomed to taking." That is a description of what learned-heuristic proof search does, written by the person usually cited as having disproved the approach.

And then the reinstatement, which is why this entry earns its place. On 25 July 2024 Google DeepMind reported AlphaProof, "a system that trains itself to prove mathematical statements in the formal language Lean," coupling a pre-trained language model with the AlphaZero reinforcement-learning algorithm and "searching over possible proof steps in Lean." With AlphaGeometry 2 it solved four of six 2024 International Mathematical Olympiad problems for 28 points out of 42, one short of the gold threshold; the method was published in Nature on 12 November 2025, with training on roughly 80 million auto-formalized statements. Solve times ranged from "within minutes" to "up to three days." That is LT's architecture exactly — incomplete search over a subproblem space in a formal system, under a budget, with no guarantee — with the one component Newell, Shaw and Simon had to write by hand replaced by a learned function.

So the full grade on the central bet is: wrong on its due date, right on a mechanism the authors could not supply. Hand-written heuristics lost to a complete decision procedure in 1960 because nobody could write good enough heuristics by hand. Heuristic search came back once the heuristic stopped being written by hand. Read shannon-chess-1950 beside this and the two arcs are the same arc, sixty years long, in two domains, which is stronger evidence than either alone. A reading that quotes only Wang gets "heuristics were a dead end"; a reading that quotes only AlphaProof gets "Newell and Simon were right all along." Both are half a record, and the half that matters is the middle.

The prediction that belongs to this entry, graded. In 1957 Simon delivered a paper co-authored with Newell to the Operations Research Society of America, published as "Heuristic Problem Solving: The Next Advance in Operations Research" in Operations Research Vol. 6, No. 1, January–February 1958, pages 1–10. It contains four dated claims. shannon-chess-1950 already grades the first (world chess champion within ten years; due 1967, achieved 1997, thirty years late). The second is this entry's:

> That within ten years a digital computer will discover and prove an important > new mathematical theorem.

Made 1957. Due 1967. What actually happened: nothing by 1967, and nothing that counts for nearly thirty years. The Four Colour Theorem fell to Appel and Haken in 1976 with machine assistance, but the machine checked cases a human had enumerated — it did not discover the proof. The clean cash-out is 10 October 1996, when William McCune's EQP at Argonne found a proof of the Robbins conjecture, open since the early 1930s, after about eight days of search on an RS/6000 using roughly 30 megabytes. That is a program discovering and proving a theorem that mathematicians had wanted and failed to get. Twenty-nine years late. On the softer reading — a theorem important enough that the field reorganises around it — the claim is arguably still open in 2026, and the Crouzeix items in the current window are the test case, which is precisely why they are worth this entry's discipline rather than its enthusiasm.

There is no newell-simon-1958 entry in canon/ and no line for it in proposals.md. There should be; the four claims are a base rate in a single paragraph, from the two people best placed to know, made at the exact moment their program was working. I have the wording at second hand from a secondary quotation of the printed text and have not read the journal article. Anyone writing that entry should check it against Operations Research before quoting.

Wrong in a way that is nobody's fault: "the first AI program." The claim is made routinely, was made by the authors' allies rather than mainly by the authors, and does not survive contact with the record. Christopher Strachey's draughts program and Dietrich Prinz's chess program both ran in 1951; Arthur Samuel's checkers program was running by 1952 and was heuristic, and Shrager's 2026 paper concedes the point in a footnote — Samuel's "existed a couple of years before LT, and it too was heuristic," and "might arguably be the first machine learning program, and the first system to learn from self-play." What distinguishes LT is not primacy in time. It is that Samuel set out to build a checkers player and Newell, Shaw and Simon set out, in Shrager's phrasing, "to model human cognition across many domains" — the first program written as an instance of a general theory rather than as a solution to its task. That is a defensible claim and it is the one to make.

Commonly misused as

Not required for idea. Four misuses are frequent enough, and load-bearing enough in arguments the readings adjudicate, to be worth policing.

**"It proved 38 of the first 52 theorems of Principia."** True as stated and false as understood. LT was given the axioms plus every previously proved theorem of chapter 2 at each step, "regardless of whether LT had proved the theorems itself." It did not work through the chapter; it was walked through the chapter. Seventeen of the 38 were one-step substitutions the authors themselves called corollaries. The correction is one sentence and it generalises directly to any modern claim of the form "the model solved N of M": ask what was in context.

"It was the first AI program, demonstrated at Dartmouth in 1956." LT was described at Dartmouth in the summer of 1956, not demonstrated; on Shrager's reconstruction of the versions it was "essentially specified," hand-simulated only, and did not run on a machine until IPL-II was working on the JOHNNIAC in late 1956 and early 1957. The hand simulation itself is January 1956, with Simon's wife, three children and some graduate students each holding a card and acting as a component of the program — a good story, told by Simon, and not a machine result. Primacy is contested besides; see above. A reading that wants the Dartmouth fact should say the meeting had a paper design and a hand simulation, which is a more interesting fact anyway.

**"It found a proof better than Russell and Whitehead's, and the Journal of Symbolic Logic rejected it because a computer was listed as a co-author."** The first half is well attested at second hand: LT produced a shorter proof of theorem 2.85 than the published one, and Simon showed it to Bertrand Russell, who "responded with delight." Note that 2.85 lies beyond the first 52 theorems, so this is a separate result from the 73% figure and should not be reported as part of it. The second half has grown in the telling. The recorded ground for rejection is that a new proof of an elementary theorem was not notable; the "they failed to notice the co-author" gloss is an inference added by retellers, not a documented editorial statement. I have the whole episode at second and third hand — McCorduck and Crevier, quoting Simon's recollection — and could not reach the primary correspondence. A reading may use it as an anecdote about how novelty gets classified, and should not use it as evidence of institutional hostility to machine authorship, which is not established.

"LT shows that formal systems can be mechanised" — or the mirror image, that its failures show they cannot. LT worked in a decidable fragment, badly, next to a decision procedure that its own authors named in advance. It bears on no limit result. godel-incompleteness-1931 and turing-halting-1936 are untouched by anything in these papers, in either direction, and the fact that LT's subject matter is the book in Gödel's title is a coincidence of subject matter, not a connection of substance. The one genuine limit LT demonstrated is its own: theorem 2.13 is unprovable by LT's four methods, for a stated reason, which is a fact about a program and not about logic.

Sources

Primary, read directly:

• Allen Newell and Herbert A. Simon, The Logic Theory Machine: A Complex Information Processing System, The RAND Corporation, P-868, 12 July 1956 (revised); presented at the IRE Symposium on Information Theory, Cambridge, Massachusetts, 10 September 1956; published in IRE Transactions on Information Theory IT-2, No. 3, September 1956, pp. 61–79. Read from the scan at http://www.bitsavers.org/pdf/rand/ipl/P-868_The_Logic_Theory_Machine_Jul56.pdf. All quotations of the specification, the algorithm/heuristic distinction, the Kalin-Burkhart passage and the Shaw footnote are from this text.
• A. Newell, J. C. Shaw and H. A. Simon, Empirical Explorations of the Logic Theory Machine: A Case Study in Heuristic, The RAND Corporation, P-951, 14 March 1957 (revised; internal date stamp 11 January 1957); presented at the Western Joint Computer Conference, Los Angeles, 28 February 1957; published in the Proceedings of the Western Joint Computer Conference, 1957, pp. 218–230. Read from http://www.bitsavers.org/pdf/rand/ipl/P-951_Empirical_Explorations_Of_The_Logic_Theory_Machine_Mar57.pdf. All performance numbers, the British Museum algorithm, the needle/haystack passage, the plateau paragraph and theorem 2.13 are from this text.
• Allen Newell, The Chess Machine: An Example of Dealing with a Complex Task by Adaptation, The RAND Corporation, P-620, December 1954; Proceedings of the 1955 Western Joint Computer Conference, pp. 101–108. Read from bitsavers for the reference list (item [1] is Shannon 1950), the consequences/horizon/ evaluation problems, and the goal-subgoal reinforcement scheme.
• Hao Wang, "Toward Mechanical Mathematics", IBM Journal of Research and Development, Vol. 4, No. 1, January 1960, pp. 2–22. Read from the scan at http://www.bitsavers.org/pdf/ibm/IBM_Journal_of_Research_and_Development/041/ibmrd0401B.pdf. The epigraph, all timing comparisons, the butcher's-knife passage, the "heuristic"/"strategy" passage and the "buying originality with plodding" line are from this text.
• Jeff Shrager, Executable Archaeology: Reanimating the Logic Theorist from its IPL-V Source, arXiv:2603.13514v1, 13 March 2026. Read in full: the version table, the statement that LT was not running at Dartmouth, the effort limits, the IPL-versus-Lisp comparison, the Samuel footnote, and the account of the J74 bug found by comparing the modern implementation against Shaw's original 1962 punched-card deck. The reanimated program proves 16 of 23 attempted theorems, which the paper calls historically consistent with the original's behaviour within its search limits.

Secondary and corroborating:

• Google DeepMind, "AI achieves silver-medal standard solving International Mathematical Olympiad problems", 25 July 2024, for AlphaProof, Lean, the AlphaZero coupling, the 28/42 score and the solve times; and "Olympiad-level formal mathematical reasoning with reinforcement learning", Nature, 12 November 2025, doi:10.1038/s41586-025-09833-y, for the roughly 80 million auto-formalized training statements. The Nature article itself is behind an authentication redirect; the figures above come from the DeepMind post and from Nature's own press release, and are the vendor's numbers.
• Herbert A. Simon and Allen Newell, "Heuristic Problem Solving: The Next Advance in Operations Research", Operations Research Vol. 6, No. 1, January–February 1958, pp. 1–10, for the four ten-year predictions. Second hand; see the caveat above.
• Pamela McCorduck, Machines Who Think, 2nd ed., 2004, at pp. 138 and 167, and Daniel Crevier, AI: The Tumultuous History of the Search for Artificial Intelligence, 1993, at pp. 45 and 146, for Feigenbaum's recollection of Simon's January 1956 classroom announcement, the January 1956 hand simulation, theorem 2.85, Russell's reaction and the Journal of Symbolic Logic rejection. All of this reaches this entry through secondary citation; I read neither book.
• Argonne National Laboratory's account of EQP and the Robbins problem, for the 10 October 1996 date, the eight-day search and the machine used.

Noted failures, per the discipline:

• The RAND Corporation's own page for P-868 returned HTTP 403 on 2026-08-16, as did a first attempt at the bitsavers copy through a mirror; the successful reads are recorded above.
• The Bertrand Russell Journal (McMaster) carries an article built around the Simon–Russell correspondence — the title begins "Dear Earl Russell: Mr. Newell and I thought you might like…" — which is the primary source for Russell's reply and probably for the Journal of Symbolic Logic episode. Both the article page and its PDF returned an access-denied error on 2026-08-16. The section above is written without it, and it is the single item that would most improve this entry.
• E. Stefferud, The Logic Theory Machine: A Model Heuristic Program, RAND RM-3731-CC, 1963 — the complete IPL-V listing Shrager worked from — was not read. Everything about the 1963 version here is Shrager's report of it.
• I did not reconcile Shrager's per-theorem results table against the raw run log published with the paper; the counts I could read off each did not agree, and the figure quoted above is the one stated in the paper's own abstract and text.

This entry places no needle, no score and no landmark, and deposits nothing in the evidence ledger.