AM: An Artificial Intelligence Approach to Discovery in Mathematics as Heuristic Search

TL;DR — In 1976 Douglas Lenat built AM, a program that started from ~100 set-theory concepts and, guided by hand-written "interestingness" heuristics, autonomously reinvented numbers, arithmetic, primes, and a version of Goldbach's conjecture — then stalled after a few hundred concepts and never recovered. Fifty years on, every missing ingredient exists: LLMs supply the mathematical prior AM lacked, Lean supplies the grounding it never had, and FunSearch-style loops prove the search recipe scales. AM is the cleanest spec ever written for open-ended machine discovery, and it is now buildable.

The idea as Lenat had it

AM was not a theorem prover. It didn't solve posed problems at all. It was a program whose only job was to decide what is worth thinking about next — Lenat framed mathematical discovery itself as heuristic search over a space of concepts.

The machinery, from his Stanford PhD thesis (later published as Stanford AI Lab memo AIM-286 and in the Davis & Lenat book Knowledge-Based Systems in Artificial Intelligence):

• Concepts as frames. Roughly 115 seed concepts (sets, set operations, equality, composition…), each a frame with a couple dozen slots: definition (as Lisp code), examples, generalizations, specializations, analogies, conjectures, and a numeric worth.
• An agenda of tasks. Things like "fill in examples of Set-Equality" or "check extreme cases of Divisors-of," each with a priority computed from the worth of the concepts involved and the reasons the task was proposed.
• ~250 heuristics. Condition–action rules attached to concepts, encoding a folk theory of mathematical taste: if a predicate is rarely true, define the set of things satisfying it and study that; if two independently-derived concepts coincide, that's interesting; look at extreme cases; if f(x,x) is interesting, name it as a new unary operation.

The loop: pop the top agenda task, fire applicable heuristics, which create examples, new concepts, new conjectures, and new tasks; update worth; repeat.

The famous run is genuinely striking. Starting from sets, AM specialized "equality of bags" into "same length," which became cardinality, i.e., natural numbers. Bag union and bag-of-bags flattening became addition and multiplication. Inverting multiplication gave divisors. The extreme-case heuristic applied to divisors ("which numbers have very few?") produced primes; the opposite extreme produced highly composite numbers — which Lenat noted Ramanujan had studied. Empirically tabulating sums of pairs of primes surfaced Goldbach's conjecture. All of this without any of those concepts being coded in.

Why it could not work then

The plateau. After roughly 200 new concepts, AM's output degraded into junk — concepts Lenat couldn't recognize as mathematics and worth ratings that stopped discriminating. His own diagnosis (in the 1984 paper with John Seely Brown, "Why AM and EURISKO Appear to Work") is the honest one: the heuristics were tuned for the neighborhood of the seed concepts. As AM moved from set theory into number theory, they gradually lost relevance, and AM had no way to invent new heuristics because heuristics weren't themselves concepts it could operate on.

The Lisp trick. Ritchie and Hanna's 1984 critique, which Lenat partly conceded, identified a subtler issue. AM's concept-mutation heuristics did small syntactic edits on Lisp definitions, and this worked because Lisp's syntax was unusually well aligned with mathematical semantics — deleting a conjunct of a short lambda expression tends to yield a meaningful generalization. That was a fortunate coincidence of representation, not a general theory of concept formation. Change the domain and the trick dies. AM had, in modern language, no prior over mathematics beyond what was smuggled into 115 frames and the structure of Lisp.

No grounding. AM never proved anything. "Conjectures" were empirical regularities over a handful of small examples, and "interestingness" was hand-set numbers combined by hand-set formulas. Ritchie and Hanna also documented that the clean published run involved considerable human steering and parameter fiddling; unattended runs were much less impressive.

Raw scale. AM ran on the Stanford AI Lab's PDP-10 — roughly 1 MIPS and on the order of a megabyte of usable memory. The whole concept space had to fit in core; a run was hours of CPU for a few hundred concepts, each examined via dozens of tiny examples. There was no room for wide search, no room for a large knowledge base, and certainly no room to learn the interestingness function rather than hand-code it.

What changed

Each of AM's three fatal gaps now has a direct fix.

The prior. An LLM trained on the mathematical internet is exactly the "rich prior over mathematics" AM lacked. It can propose definitions, name them sensibly, guess which specializations are fruitful, and — crucially — its proposals degrade gracefully outside the seed neighborhood instead of collapsing, because the prior covers all of human mathematics rather than one hand-coded region. The Lisp-syntax trick is replaced by sampling from a distribution over meaningful mathematical text.

The grounding. Lean 4 with mathlib gives what AM never had: a machine-checkable notion of a well-formed definition, a true theorem, and a counterexample. Conjectures can be attacked by counterexample search (property-based falsification, decide on decidable fragments) and by learned provers. AlphaProof's 2024 IMO silver-medal performance showed LLM-guided formal proof works at a serious level.

The loop at scale. FunSearch (DeepMind, published in Nature, late 2023) is structurally AM's loop with the substitutions made: LLM as the mutation heuristic, a programmatic evaluator as the worth function, an evolutionary archive as the agenda. It produced a new lower bound for the cap set problem — a genuinely new mathematical object — and AlphaEvolve (2025) extended the recipe across dozens of problems, including improving a matrix-multiplication algorithm. The recipe is validated; what FunSearch does not do is invent concepts. It optimizes a fixed scoring function on a fixed problem. AM's ambition was strictly larger: open-ended growth of the concept space itself.

Interestingness can be learned. The one component everyone assumed was hopelessly subjective turns out to be tractable: work in the open-endedness community (e.g., OMNI, Jenny Zhang, Lehman & Clune, 2023) uses an LLM directly as a model of interestingness to steer open-ended learning, and it works — LLM taste, distilled from human taste, filters novelty from noise far better than hand-coded formulas. This is a near-exact vindication of AM's most-criticized component.

A serious 2026 revival

Keep from Lenat: the agenda architecture, concepts-as-first-class-objects with worth, the taxonomy of discovery moves (specialize, generalize, compose, invert, look at extremes, notice coincidences), and the framing that task selection is the whole game. Replace everything else.

Concretely:

• Proposer: a strong LLM emitting Lean definitions and conjectures directly (skip autoformalization when possible), prompted with the current library and recent "interesting" events, with AM's discovery moves as an explicit action vocabulary.
• Grounding: Lean typechecking gates well-formedness; a falsifier (random/enumerative testing over small models) kills most conjectures cheaply; a prover attempts the survivors with a compute budget scaled to estimated worth.
• Interestingness: a learned model combining measurable signals — compression/reuse (does the new concept shorten later proofs and definitions? this is DreamCoder's library-learning objective, and the right formalization of AM's "worth"), surprise (proposer's own log-probability of the verified statement — low probability plus true is interesting), and LLM-judged taste, calibrated against mathlib's actual dependency graph.
• Scale: FunSearch-class budgets — millions of proposals, an archive maintaining diversity across areas rather than a single greedy agenda, exactly Lenat's worth-propagation generalized.

The honest success criterion: does the system, seeded only with foundations, generate concepts that working mathematicians recognize as new and worth having — not new bounds on posed problems, but new definitions that earn their place by making other things shorter?

Has it been tried, and what's open

Partially. Minimo (Poesia et al., NeurIPS 2024, "Learning Formal Mathematics from Intrinsic Motivation") is the closest direct descendant: an agent that conjectures and proves in a formal system from axioms alone, bootstrapping its own curriculum — AM's spirit with real grounding, but at toy scale and without concept/definition invention as the objective. DreamCoder (Ellis et al., 2021) solved the concept-reuse half in program synthesis. FunSearch/AlphaEvolve solved the scale half on fixed objectives. OMNI solved (or at least dented) the interestingness half. Nobody, to my knowledge, has assembled all four at scale aimed at open-ended concept invention in Lean. That's the gap, and it looks like an engineering-plus-taste problem rather than a missing-science problem.

What's still open is the question AM actually died on: whether the generator of variation itself can keep improving. Lenat's answer was EURISKO (1981–83) — make heuristics into concepts so they can be discovered too; it famously won the Traveller TCS wargame tournaments but was even more dependent on Lenat-in-the-loop, and his eventual conclusion (knowledge is the bottleneck) became the 40-year Cyc detour. LLMs answer the knowledge bottleneck, but a frozen LLM is a fixed heuristic pool with vastly better coverage — the plateau argument still applies, just further out. Whether self-generated verified mathematics can fine-tune the proposer into genuinely new taste, rather than recycling human taste, is the live question, and it's the open-endedness question in miniature.

Where to read it

The link for this piece was not provided and I haven't verified bibliographic details against the original; the thesis circulated as Stanford AI Lab Memo AIM-286 (1976), and the accessible version is in Davis & Lenat, Knowledge-Based Systems in Artificial Intelligence (McGraw-Hill, 1982). Read alongside: Lenat & Brown, "Why AM and EURISKO Appear to Work" (1984) — a rare, candid post-mortem by the author himself; Ritchie & Hanna's critique (Artificial Intelligence, 1984); Romera-Paredes et al., FunSearch (Nature, 2023) for the loop at scale; Ellis et al., DreamCoder (2021) for concept reuse as compression; and Poesia et al., Minimo (2024) for the grounded, intrinsically motivated version now taking its first steps. Together they read like a 50-year relay race in which AM ran the first leg alone, in the dark, and roughly in the right direction.