Original Blog Essay

Beyond Proof Automation: Toward LLM Mathematical Discovery Systems

Tiantian Zhang ยท Department of Computer Science, Columbia University
A statistical-learning and formal-methods view of proposal distributions, trajectory data, creative generation, ATP-aware proof search, verifiers, certificates, and human mathematical judgment.

An English original blog essay on proposal distributions, trajectory data, creative generation, ATP-aware proof search, verifiers, formal certificates, and the future of mathematical discovery.

0. Motivation: the question after proof automation

A great deal of current excitement around AI for mathematics is framed as proof automation: give the system a theorem, ask it to fill the proof, and then check the result in Lean, Coq, Isabelle, or another proof assistant. This framing is natural, but it is also too narrow. The most interesting research question is not only whether a model can close a sorry; it is whether a model can become a reliable participant in the broader process by which mathematics is discovered.

Mathematical research is not a sequence of fully specified theorem-proving tasks. It involves choosing definitions, inventing representations, finding examples and counterexamples, making analogies, decomposing a problem into lemmas, locating a hidden theorem in the literature, building toy models, and deciding which formal statement is actually worth proving. Proof is the final certificate, but the discovery process begins much earlier.

The right abstraction, therefore, is not "LLM as oracle." A more disciplined view is that a language model induces a learned proposal distribution over mathematical objects. Given a problem context $x$, the model samples candidate objects $h$: a proof sketch, a Lean file, a counterexample, a theorem statement, a lemma graph, a computation, a search trajectory, or a possible analogy. Verifiers then decide which of these candidates survive.

In this view, the central research question becomes:

What data distributions, post-training objectives, trajectory environments, creative proposal mechanisms, ATP-aware proof-search interfaces, and verifier architectures make rare but certifiable mathematical objects discoverable?

This essay develops that question. The aim is to keep the philosophy ambitious but the language statistically and formally grounded.

1. From language modeling to proposal distributions

Let $x$ denote a mathematical context: an open problem, a theorem statement, a partial Lean file, a natural-language proof draft, or a collection of related papers. Let $h$ denote a candidate mathematical object. The model does not output truth directly. It induces a conditional distribution

$$ q_\theta(h\mid x). $$

The candidate $h$ may be informal or formal. It may be a proof sketch, a conjecture, a counterexample, a finite witness, a definition, an experiment, a theorem DAG, a Lean proof, a retrieval path, or a sequence of tool calls. The model's contribution is to place probability mass on some regions of this space and little or none on others.

A useful mathematical discovery system is one in which the correct or interesting object has non-negligible effective probability under this proposal distribution, and where search and verification can amplify that probability. If the right construction has essentially zero support under $q_\theta(\cdot\mid x)$, no verifier can recover it. If it has small but nonzero support, retrieval, decomposition, latent planning, parallel sampling, formal feedback, and theorem proving can make it discoverable.

This distinction matters. It avoids two common mistakes. The first mistake is to say that a model either "knows" or "does not know" the solution. The second is to say that a verifier alone solves the problem. A verifier can reject bad candidates, but it cannot select a candidate that is never proposed. Discovery depends on the interaction between proposal quality and verification strength.

2. The target distribution is not the pretraining distribution

Pretraining fits patterns in a large data mixture: books, papers, code, websites, discussions, formal proofs, theorem statements, wrong arguments, and many kinds of partial reasoning. In a simplified form, next-token training estimates

$$ P_{\mathrm{pre}}(x_t\mid x_{<t}). $$

Mathematical discovery, however, requires a different target distribution. We might write it schematically as

$$ P_\star(d,g,c,\pi,e\mid x), $$

where $d$ represents useful definitions, $g$ represents goals or conjectures, $c$ represents constructions or counterexamples, $\pi$ represents proofs or formal certificates, and $e$ represents explanatory trajectories.

The mismatch between $P_{\mathrm{pre}}$ and $P_\star$ is central. A model can be extremely strong on familiar text patterns while still assigning too little probability to a rare counterexample, a nonstandard representation, or a proof assistant certificate. Conversely, a model can be useful for research even if it is not perfectly truthful at the language level, provided its proposals are diverse and its outputs are passed through strict verification.

This is why the question "how much data?" is incomplete. For mathematical discovery, the better question is: which distribution of data is being scaled? Static world-knowledge text produces one kind of prior. Tool-use trajectories, Lean proof states, compiler errors, failed tactics, proof repairs, theorem search logs, and formal certificates produce a different prior.

Scaling laws describe important empirical regularities in how loss changes with model size, data size, and compute. But for research-level reasoning, the decisive issue is not merely the number of tokens. It is whether the scaled distribution contains the right kinds of mathematical objects, the right failures, the right feedback, and the right certificates.

3. Scaling laws, Transformer, MoE, and what they do not explain

It is tempting to summarize frontier model progress by naming three pillars: Transformer architectures, mixture-of-experts capacity, and scaling laws. This summary is useful but incomplete.

The Transformer gives a powerful sequence-modeling architecture. MoE increases total parameter capacity while activating only a sparse subset of experts per token. Scaling laws describe how loss tends to improve as model size, data, and compute increase under certain regimes. These components matter, but they do not by themselves define a mathematical discovery system.

A more faithful capability decomposition is

$$ \text{capability} \approx F(\text{architecture}, \text{parameters}, \text{data}, \text{compute}, \text{optimization}, \text{post-training}, \text{tools}, \text{search}, \text{verification}). $$

For mathematics, the last four terms are especially important. Post-training changes model behavior. Tools give feedback. Search explores multiple candidates. Verification turns plausible language into certified knowledge. Without these layers, scale can produce fluency without reliability.

This also gives a more careful way to discuss claims about frontier labs. Unless a training recipe, parameter count, or data mixture is publicly documented, it should be treated as speculation. What can be discussed more rigorously is the structural direction: models are moving from static chatbots toward agents trained and evaluated in feedback-rich environments. In mathematics, those environments include Lean, Python, symbolic algebra systems, theorem search engines, SAT/SMT solvers, finite model finders, and human proof review.

4. From static text to trajectory data

One of the most important shifts in recent AI systems is the move from static text prediction to trajectory learning. A trajectory can be written as

$$ \tau=(s_0,a_0,o_1,r_1,s_1,a_1,o_2,r_2,\ldots), $$

where $s_t$ is the environment state, $a_t$ is the model action, $o_t$ is the observation, and $r_t$ is feedback. The trajectory distribution is roughly

$$ P(\tau)=P(s_0)\prod_t \pi_\theta(a_t\mid h_t)E(o_{t+1},r_{t+1},s_{t+1}\mid s_t,a_t), $$

where $h_t$ is the visible history and $E$ is the environment dynamics.

For coding agents, the environment may be a terminal, a test suite, a compiler, a browser, or a repository. For mathematical agents, the environment may be a proof assistant, a computer algebra system, a theorem database, or a finite search engine. The crucial property is verifier density: how often the environment can return objective, cheap, local feedback.

Lean has high verifier density. Every tactic, definition, import, coercion, typeclass instance, and lemma application can be checked. This makes it an unusually valuable environment for trajectory data. A failed proof attempt is not just a failure; it is a structured training signal. It says which local proof state was reached, what action was tried, and how the type checker rejected it.

This does not mean mathematical research reduces to Lean interaction. Many conceptual moves cannot be locally certified. But Lean-like environments make a large part of the proof-engineering process observable, and that observability is precisely what turns failures into curriculum.

5. Post-training and the shape of the research policy

Pretraining gives a base distribution. Post-training reshapes it. SFT, RLHF, RLAIF, DPO-style optimization, rejection sampling, tool-use training, and long-reasoning distillation all transform

$$ q_{\theta_0}(h\mid x) \quad \longrightarrow \quad q_{\theta_{\mathrm{post}}}(h\mid x). $$

This transformation can help research: it can improve instruction following, decomposition, self-correction, tool use, and communication. But it can also introduce unwanted biases. A model optimized to sound helpful and polished may prefer conventional explanations over risky exploration. It may avoid uncertain conjectures, suppress strange counterexamples, or present incomplete reasoning with excessive confidence.

Mathematical alignment therefore has a different flavor from ordinary chatbot alignment. A research-oriented model should not merely be agreeable. It should be calibrated, explicit about proof obligations, comfortable exposing uncertainty, willing to generate multiple competing hypotheses, and eager to seek certificates.

The desired behavior is not "always answer confidently." It is closer to:

This is scientific alignment: the model is rewarded not just for fluency, but for producing objects and trajectories that can enter a verification pipeline.

6. Creative proposal distributions: why next-token prediction may be myopic

Verification is only half of the story. Before a system can verify a candidate, it must generate one worth verifying. This is where the paper Roll the dice & look before you leap is conceptually important.

The standard autoregressive factorization is

$$ q_\theta(y\mid x)=\prod_{t=1}^T q_\theta(y_t\mid x,y_{<t}). $$

This is powerful, but open-ended creativity may require a different internal geometry. Many creative tasks require choosing a global plan before emitting local tokens. A more natural abstraction is

$$ q_\theta(y\mid x)=\int q_\theta(z\mid x)\prod_{t=1}^T q_\theta(y_t\mid x,z,y_{<t}),dz, $$

where $z$ is a latent plan, seed, analogy bridge, proof strategy, counterexample template, or global construction.

The point is not that next-token models cannot reason. The point is that local continuation can be a poor training signal for globally coherent novelty. If randomness is injected only through output temperature, it perturbs token choices locally. For discovery, randomness should often select a latent plan first, then unfold a coherent trajectory conditioned on that plan.

This matters for mathematics. A useful mathematical candidate is often not a locally smooth continuation of a textbook paragraph. It may be a strange counterexample, a finite shadow of an infinite problem, an unexpected analogy, a nonstandard encoding, a theorem DAG decomposition, or a proof path that first constructs an object and only later explains why it works.

Thus the prover-verifier picture should be extended:

$$ \text{scale/data} \rightarrow \text{post-training} \rightarrow \text{trajectory rollout} \rightarrow \text{creative proposal distribution} \rightarrow \text{search} \rightarrow \text{verification} \rightarrow \text{certificate}. $$

The key question is no longer only how to verify a candidate. It is how to train and sample from models that propose candidates worth verifying.

7. Verifiers, certificates, and the role of pipeline-math

The value of systems such as pipeline-math is that they make the verifier side explicit. The important lesson is not that an LLM should be trusted as a mathematician. The lesson is that LLM-generated reasoning can be placed inside an auditable prover-verifier pipeline.

A typical hard-verifier pipeline has the form

open problem
  -> candidate construction or proof sketch
  -> frozen definitions and theorem statements
  -> modular proof obligations
  -> Lean formalization
  -> no-statement-drift checks
  -> sorry / axiom / unsafe audit
  -> human-readable theorem

The crucial step is freezing the semantic interface. Once the theorem statement is fixed, every later proof attempt must prove that exact statement. This prevents a common failure mode in informal reasoning: statement drift, where the system gradually proves a nearby but weaker or different theorem.

Formally, we can view a hard verifier as a certificate predicate

$$ C(x,h)\in{0,1}. $$

The goal is to search within $q_\theta(h\mid x)$ for an $h$ such that $C(x,h)=1$. If Lean accepts the proof under a trusted kernel and the project passes no-sorry and no-unsound-axiom checks, the output is no longer merely plausible. It becomes a machine-checkable certificate.

This is the difference between mathematical narration and mathematical certification. The model proposes; the verifier disciplines.

8. Soft verification before hard certification

Not every candidate can be sent directly to a hard verifier. The search space is too large, and many useful intermediate objects are informal. This is where LLM-as-a-Verifier-style systems are useful. They do not replace Lean. They provide a soft selection layer before expensive certification.

If a verifier model assigns a score $V(x,h)$ to a candidate, it induces a tilted distribution

$$ q_{\theta,V,\beta}(h\mid x)\propto q_\theta(h\mid x)\exp(\beta V(x,h)). $$

When $V$ is an LLM judge or a heuristic score, this is soft reweighting. When $V$ is a proof assistant, an executable test, or an exact computation, it becomes closer to hard truncation:

$$ q_\theta(h\mid x,C=1). $$

The architecture should therefore be layered. A generator proposes many candidates. Tool environments expand them into trajectories. Soft verifiers rank them cheaply. Hard verifiers certify the survivors. Human experts judge significance, elegance, novelty, and whether the result is mathematically worth caring about.

This separation is important. A soft verifier is allowed to be imperfect if it is used only to prioritize search. A hard verifier is not allowed to be impressionistic; it must define a trusted certificate.

9. AI4Math, Aristotle, AlphaProof Nexus, and what current systems suggest

Recent systems point toward a common architecture: informal reasoning, theorem retrieval, formal proof search, tool feedback, and proof assistant verification are being integrated into long-horizon agents.

AI4Math-style systems such as Rethlas and Archon illustrate one version of this pattern. One agent searches and reasons informally over mathematical literature; another translates the resulting proof blueprint into Lean and resolves proof obligations. The research interest is not merely that an agent writes code. It is that theorem retrieval, informal construction, formal task decomposition, and machine-checkable certification form a pipeline.

Aristotle-like systems represent another direction: long-horizon formal proof agents that combine natural-language reasoning with Lean feedback. Even when a natural-language proof draft is available, the formalization task remains difficult. The system must map mathematical concepts to library APIs, resolve coercions, discover missing lemmas, manage typeclass inference, and repair proof states.

AlphaProof Nexus and similar multi-agent proof-search systems suggest that even relatively simple loops around a strong base model and Lean feedback can solve nontrivial formal tasks, while more specialized orchestration may improve efficiency, reliability, and variance. This is a useful lesson: frontier base models already provide strong priors, but scalable research infrastructure still requires better proof-state memory, theorem retrieval, typed actions, parallel search, and failure-to-data conversion.

OpenAI's unit-distance result illustrates a complementary path. Some discoveries may begin in natural language or computational construction rather than in Lean. In that route, expert review or symbolic computation may provide the initial certificate, with formalization coming later. A mature mathematical discovery system should support both directions:

formal-first route:
formal statement -> Lean proof search -> machine-checked certificate

idea-first route:
natural-language exploration -> construction or proof idea -> expert/computational review -> optional formalization

The two routes should eventually close into one loop.

10. Autoformalization is not the same as theorem discovery

A reliable natural-language proof draft changes the nature of the problem. With a good draft, the task is often proof autoformalization: translate the argument into Lean, fill gaps, locate library facts, and repair proof states. Without such a draft, the task is formal proof search or mathematical discovery.

These regimes should be distinguished:

Regime Given Main difficulty Typical certificate
Proof autoformalization Theorem statement plus reliable informal proof sketch Translation, library mapping, gap filling, tactic synthesis, proof repair Proof assistant kernel
Formal proof search Formal statement, possibly weak hints Lemma invention, induction choice, premise selection, instantiation, search control Proof assistant plus ATP/tool feedback
Mathematical discovery Informal problem context Choosing the right statement, object, definition, counterexample, or proof strategy Mixed: human review, computation, formalization

This distinction also reveals a neglected issue: proof-code quality. If the only goal is to verify a theorem, an ugly proof may be enough. But if the goal is to build a reusable formal theory, quality matters. Definitions should be natural. Lemmas should be reusable. Proofs should be modular. Dependencies should be minimal. The resulting library should support future work.

Beyond proof automation therefore includes formal library engineering. It is not enough to close a sorry; the system should help build mathematical infrastructure that humans and future agents can extend.

Many LLM-for-Lean systems still treat formal proving as code generation. The model emits tokens, Lean accepts or rejects the result, and the agent tries again. This is effective because modern coding agents are strong, but it is not the best proof-search interface.

The mismatch is clear. A proof state is typed, structured, and constraint-based. A language model's action space is all possible tokens. The model can waste probability mass on syntactically invalid code, ill-typed terms, irrelevant theorem names, or tactics that fail only after a long generated script. The reward is sparse and delayed.

Traditional automated theorem proving developed many techniques for reducing this search space. They should be reintroduced as first-class components.

11.1 Unification and metavariables

A common proof-search difficulty is instantiating a universally quantified theorem with the right term. Rather than guessing the full term immediately, ATP systems introduce metavariables and let later constraints determine them. This is unification.

Proof assistants already support metavariables and elaboration constraints, but human-written tactic scripts often hide the underlying search dynamics. A model trained only on final scripts learns the surface record of proof, not the process by which a proof was found. A better interface would let the model propose lemma schemas, tactic families, or premise candidates while the proof assistant handles metavariable constraints and prunes impossible branches.

11.2 Term indexing and premise selection

Large formal libraries create a premise-selection problem. Instead of asking the model to hallucinate theorem names from the entire library, symbolic indexing can retrieve shape-compatible facts using discrimination trees or related structures. The neural model can then rerank a typed candidate set.

This is a better division of labor. Symbolic infrastructure handles exact matching and indexing; the LLM supplies semantic prioritization, analogy, and high-level strategy.

11.3 Sledgehammer-style hybridization

Isabelle's Sledgehammer tradition shows the value of connecting high-level proof assistants to external ATP and SMT solvers. A similar hybrid strategy is attractive for LLM-based systems:

LLM proposes decomposition and relevant context
  -> symbolic ATP/SMT handles local obligations
  -> proof assistant reconstructs and checks proof
  -> failures return to the LLM and the training loop

The future is unlikely to be pure neural theorem proving or pure symbolic theorem proving. It is more likely to be neural guidance over structured symbolic search.

12. Self-play and synthetic mathematical curriculum

Formal proof data is scarce. One way to expand it is self-play: let one component generate conjectures and another try to prove them. The conjecturer should generate statements that are novel, meaningful, and barely within the prover's reach. The prover attempts proofs. The verifier supplies the reward. The resulting successes and failures become training data.

A simple proxy is to search for short statements with long proofs. Short statements are compressed; long proofs indicate nontriviality. But this proxy is insufficient on its own. Many short hard statements are artificial. A useful self-play curriculum must also account for novelty, naturalness, downstream reuse, theorem-DAG centrality, resistance to degenerate artifacts, and human mathematical taste.

The loop is nevertheless promising:

conjecture generation -> proof attempt -> verifier feedback -> difficulty calibration -> training data -> stronger prover and conjecturer

If this loop is combined with Lean proof states, ATP search traces, retrieval paths, counterexample finders, and proof repair logs, it becomes a scalable curriculum for mathematical agents.

13. Hallucination as misweighted association

Hallucination is often treated as a defect separate from reasoning. For mathematical discovery, it is better understood as a failure mode of the same associative machinery that enables useful recombination.

Subsequence-association theories of hallucination suggest that a model may follow a strong local association even when the global context contradicts it. In mathematics, the model may learn patterns such as:

finite conductor -> quasi-coherent
integer-valued polynomial ring -> closure under multiplication
tensor product map -> canonical isomorphism
quotient ring with nilpotents -> counterexample pattern

These associations can be useful in ordinary contexts and misleading near the boundary of an open problem. The generator may propose a plausible but false lemma because a familiar local pattern dominates a rarer faithful structure.

This connects directly to creative generation. Hallucination is local association without truth discipline. Weak creativity is local prediction without latent global planning. Weak agency is action generation without feedback-calibrated trajectories. A reliable discovery system needs all three corrections: better global proposal mechanisms, better environment feedback, and stronger verification.

14. What internal structure do frontier LLMs learn?

A reasonable hypothesis is that frontier LLMs do not store mathematics as a theorem database. They learn a compressed, entangled, probabilistic atlas of mathematical language, code, proof motifs, symbolic transformations, library conventions, and tool-use trajectories.

The learned structures may include:

Mechanistic interpretability gives partial tools for studying these structures: induction heads, superposition, sparse features, and circuit analysis. But mathematics requires more task-specific questions. Which circuits support symbolic binding? Which features encode algebraic construction patterns? Which prompt subsequences trigger false lemma hallucinations? Which proof-state trajectories teach repair? Which latent seeds yield coherent but novel theorem candidates?

Benchmark accuracy alone cannot answer these questions. We need to connect interpretability, data distribution analysis, formal verification, and failure mining.

15. Failure modes and interventions

When a model fails on an open problem, the unhelpful diagnosis is "the model is not smart enough." A better diagnosis asks which bottleneck failed.

Failure mode Meaning Possible intervention
Support failure The correct object is nearly absent from $q_\theta(\cdot\mid x)$ Targeted data, retrieval, domain finetuning, library expansion
Search failure The object has small probability but was not sampled Best-of-N, tree search, theorem DAG decomposition, parallel sampling
Creative proposal failure Candidates are repetitive or locally plausible but not original Multi-token objectives, diffusion-style generation, seed-conditioning, latent-plan sampling
Trajectory failure The environment gives too little useful feedback Lean/Python/CLI rollouts, richer tool environments, better logging
Verifier failure Bad candidates pass or good candidates are rejected Stronger verifiers, adversarial tests, formal certificates, calibration
Proof-search interface failure The model must generate raw tactic tokens in a huge action space ATP-aware APIs, typed actions, metavariables, unification, term indexing
Retrieval failure The key theorem, paper, or library lemma is not found Theorem search, citation graph search, semantic retrieval, premise selection
Representation failure The problem is encoded in an unhelpful form New definitions, finite shadows, alternate formalizations, abstraction design
Alignment failure Post-training rewards polish over exploration Research-oriented SFT/RLHF, uncertainty calibration, failure-trace training
Library failure The formal ecosystem lacks the needed abstraction Mathlib contributions, reusable lemma mining, API design
Significance failure The result is formally true but mathematically uninteresting Human taste, novelty filters, downstream reuse metrics

This table is meant to change the research conversation. The question is not whether the model is mystical or useless. The question is where the pipeline loses the rare certifiable object.

16. Toward a closed-loop discovery infrastructure

The long-run goal is a closed-loop system:

pretraining / post-training / synthetic data
        -> agent trajectory rollouts and proof-state data
        -> creative proposal model q_theta(h|x)
        -> seeded or multi-token sampling
        -> theorem retrieval and ATP-aware proof search
        -> soft verifier ranking
        -> hard formal verification or computation
        -> certificate or failure trace
        -> failure mining, active data, and library expansion
        -> updated model, tools, and formal ecosystem

In this loop, failure is not waste. Lean errors, failed proof states, wrong counterexamples, overstrong statements, bad retrieval paths, missing library lemmas, compiler failures, and false analogies all become data. The formal library becomes shared memory. The verifier stack becomes the discipline. The model becomes a proposal mechanism. Human researchers steer abstraction, taste, and significance.

This is a different vision from simply asking a chatbot for a proof. It is a research infrastructure in which models, tools, verifiers, data, and humans co-evolve.

17. What lies beyond automating proof?

If proof automation means "given theorem, find proof," then beyond proof automation includes at least the following:

The deepest question is not whether AI can write proofs. It is whether we can build a reliable discovery process in which statistical models generate possibilities, formal systems impose truth, and human researchers guide meaning.

18. A sharpened research question

We can now state the research program more precisely.

Given a problem context $x$, a candidate space $\mathcal H$, a proposal distribution $q_\theta(h\mid x)$, a latent-plan distribution $q_\theta(z\mid x)$, a trajectory environment $E$, a soft verifier $V(x,h)$, and a hard certificate predicate $C(x,h)$, how does the probability of discovery change with search budget $B$?

Let $\mathcal S_B(x)$ be the set of candidates produced under budget $B$. We want to understand

$$ p_B(x)=\Pr[\exists h\in\mathcal S_B(x): C(x,h)=1]. $$

In the simplest independent-sampling approximation, if a single sample succeeds with probability $p$, then

$$ p_B\approx 1-(1-p)^B. $$

But the real problem is that $p$ is not fixed. It depends on data support, model scale, post-training, trajectory data, creative generation objectives, seed-conditioning, retrieval, theorem DAG decomposition, ATP-aware proof search, verifier calibration, formal library coverage, failure traces, and human abstraction design.

This is the value of the framework. It turns the vague question "Can LLMs solve open problems?" into a set of components we can analyze, improve, and test.

19. Conclusion

The emerging evidence from pipeline-math, LLM-as-a-Verifier, AI4Math-style Rethlas/Archon systems, Aristotle-like formal agents, AlphaProof Nexus-style orchestration, unit-distance-style construction discovery, self-play theorem proving, hallucination theory, and creative-generation work all point in the same direction.

The future of LLMs in mathematics is not merely automated proof. It is the construction of a discovery infrastructure:

Models generate diverse and original mathematical candidates; trajectory environments provide feedback; ATP-aware interfaces reduce combinatorial waste; verifiers impose truth; failures become curriculum; formal libraries become shared memory; human researchers guide abstraction and significance.

That is the philosophy I find most compelling. The model does not replace mathematical truth. It proposes possible paths through a vast search space. The verifier does not create ideas by itself. It filters and certifies. The human does not disappear. The human increasingly designs the problem interface, the curriculum, the formal ecosystem, and the notion of mathematical significance.

Beyond proof automation is the study of how all of these pieces can form a reliable process of discovery.

References and pointers