Machine learning and information theory concepts towards an AI Mathematician

In plain words

This is an essay, not a system with results. The authors ask what a computer would need to be optimised for in order to discover interesting mathematics, rather than only proving theorems that people have already stated.

Their main idea is borrowed from compression. A good body of theorems is small to write down, yet lets you reach many other true statements in a few logical steps. A new theorem is worth keeping if adding it makes that body more compact and more powerful. Surprising results count as useful, because they teach the system something its current predictions did not know.

The essay then sketches how such a system could search for conjectures and prove them with the same kind of goal-directed learning used in game-playing agents. It leaves most of the details open.

TL;DR

• Position paper: no implementation, no experiments, no numbers to reproduce.
• Core hypothesis: a theorem t is useful in proportion to how efficiently the current theorems plus t compress the set of all provable statements §6.
• Practical proxies proposed: a description-length penalty, surprise under the current model, sampling conjectures in proportion to a reward, and proof search with lemmas as subgoals §6 §7 §8 §9.
• Relevant if you are designing an objective for automated theorem discovery or conjecture generation. It gives no algorithm you can run as written.

Problem

Current deep learning is described as strong at fast, intuitive ("system 1") pattern use and weaker at deliberate reasoning and calibrated uncertainty ("system 2") §1 §2. Imitation of human-written proofs gives no signal from statements that have no proof supplied §9. The essay asks what training objective could drive discovery of new, interesting theorems without human labels of interestingness §6. It notes that screening all statements is not feasible, and random sampling would rarely hit provable ones §8.

Method

The paper proposes ideas and a research direction. It defines no algorithm, loss or reward function. The pieces below are its proposals, each with its section.

1. State as a proof graph. Each node is a true statement. An edge says how a statement is derived from its parents. A proof is a connected subgraph that ends in the new theorem §5. Some nodes are marked as theorems, the set T(S). Only these are reused as premises for new proofs, while intermediate lemmas are not §5.

2. Usefulness as compression. A theorem t is useful relative to the current theorems T(S) if T(S) together with t can derive many provable statements beyond S within at most k derivation steps. The description length of T(S) also counts §6. The paper gives no formula for k, for description length or for the number of statements covered.

3. Bayesian prior on description length. A theory needing n fewer bits than a rival, and explaining the data equally well, is preferred by a factor of 2^n §3. Bits are the negative log prior probability §3.

4. Surprise as a signal. After a theorem is proved, a low prior probability P(t | T(S)) under the system's own intuition suggests the theorem is worth adding §7. Before a proof is found, the expected surprise of the truth value of t is proposed as a measure of how valuable a search for a proof or a counterexample would be §7.

5. Conjecture sampling. Train a generative model of structured objects so that it samples a statement t with probability proportional to a reward R(t) measuring usefulness. The paper prefers this to reinforcement learning, which targets a single maximiser of R §8.

6. Proof search with subgoals. Use goal-conditioned reinforcement learning: the policy takes the goal as input and the reward depends on it §9. Learn intermediate lemmas as subgoals, in the spirit of hierarchical RL and planning §9. Pre-train on an existing library of theorems, then explore without supervision §9 §10.

7. Compression of definitions. A symbol or definition that is used more than once in a set of statements already compresses that set, so it is a candidate for inclusion §9. The paper points to earlier work on identifying repeated structure in existing proofs §9.

Key expression, the expected-surprise estimate of a statement's truth value §7. The paper has no numbered equations; the expression is inline text.

\mathbb{E}_{P(t \mid T(S))}\left[-\log P(t \mid T(S))\right] §7

Sketch of the loop the essay implies. This is not an algorithm from the paper; it is assembled from §6, §8 and §9:

# Sketch assembled from [§6] [§8] [§9]; the paper gives no algorithm.
# Input:  theorems T (set of proven statements), reward R (usefulness)
# Output: new proven theorems added to T

def discovery_round(theorems, reward_model, prover):
    # Sample candidate conjectures in proportion to reward  [§8]
    conjectures = sample_proportional_to(reward_model, theorems)

    for conjecture in conjectures:
        # Search for a proof using subgoal lemmas  [§9]
        proof = prover.search(goal=conjecture, premises=theorems)
        if proof is found:
            # Keep it if it compresses the body of theorems  [§6]
            if reward_model.score(conjecture, theorems) > 0:
                theorems = theorems | {conjecture}

    return theorems

Hyperparameters

The paper reports no experiments and no training hyperparameters.

Results

No experimental results are reported. The paper contains no tables, no benchmarks and no measured numbers. The only quantitative statements are conceptual, such as the 2^n factor between theories that differ by n bits §3.

Paper vs code

No official code.

The LaTeX source contains no code link and no project-page link. The raw arXiv metadata has no comments field to check. A GitHub repository search for "AI mathematician" and for "conjecture generation bengio" returned only unrelated repositories whose owners are not the paper's authors.

Pitfalls

• Nothing to run. The essay has no method to implement. An agent that takes it as a spec must invent k, R(t), the description length and the prover. The paper leaves all four open §6 §8.
• Interestingness is not defined. The paper says the objective should not need human labels of interestingness, yet suggests pre-training on theorems that humans find interesting §6. The two are in tension and are not resolved.
• Compression is not measured. Description length of T(S) is named but not computed, and the paper notes that a single conjunction of many theorems could have about the same description length as the set itself §6.
• Surprise can reward junk (our reading). The surprise and entropy heuristics §7 do not say how a surprising theorem is separated from a surprising but useless one. Only the compression term §6 could filter such statements, and the paper does not show that it does.
• Maximum-likelihood caveat. The paper says training an LLM is in practice a regression to observed frequencies in a finite corpus, not a direct estimate of provability §4 (in a footnote). Predictions of P(x in M) from a trained model are therefore estimates of "language-likeness", not proof statistics §4.
• Lemma reuse. The paper argues that only theorems, not intermediate lemmas, should be reused as premises §5. It also says that names for lemmas make proofs compact and proposes that definitions used more than once should be kept §9. These two positions can conflict and the paper does not say how to choose between them.
• Working-memory constraint is untested. The idea that each derivation should involve only very few antecedents is proposed as something to test, not as a finding §5.
• Section numbers are from the source. The LaTeX uses amsart, which numbers sections automatically. The numbers above were counted from the source order (§1 Context to §10 Conclusion) and were not checked against the compiled PDF.

Lineage

• Builds on: prior work the paper cites on working memory and inductive biases, generative flow networks, proof assistants such as Lean and Coq, and the mathlib library. None of these has a card in this wiki yet.
• Compared against: none. The paper compares no method.
• Superseded by: not applicable.