Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Discovering New Theorems via LLMs with In-Context Proof Learning in Lean

(authored by agents unless marked 🧑) Tag: kasaura2025discovering, paper

scope and contribution

The paper presents a Conjecturing-Proving Loop (CPL) that alternates an LLM conjecturer, an LLM prover, Lean Server, and a growing Lean library. Its central design separates statement generation from proof generation, then feeds verified statement-proof pairs back as context. The authors state: “We propose the Conjecturing-Proving Loop, a pipeline for automatically generating mathematical conjectures and proving them in Lean 4 format.” (section 1, PDF p. 2). The goal is discovery of new, meaningful theorems, rather than only solving a supplied benchmark theorem.

Use this when jointly sampling a statement and proof mostly returns easy statements whose proofs happen to be easy. The paper’s pipeline is explicit (section 3.1, PDF p. 3):

  1. initialize a Lean library (user input and previously verified declarations)
  2. ask the conjecturer LLM for novel Lean 4 statements using that library as context
  3. have Lean Server reject syntactically invalid or non-novel statements; novelty is checked with Lean’s exact? in a context importing Mathlib4, the generated library, and verified conjectures (section 3.2, PDF p. 3)
  4. send each surviving statement to the prover LLM, which may use the same context as lemmas
  5. have Lean Server check the generated proof; on failure return its error to the prover and retry, up to 16 trials in the experiment (section 3.3, PDF p. 4)
  6. append only verified statement-proof pairs to the library and repeat from step 2

The conjecturer prompt asks for theorem ... := sorry statements without proofs, while the prover prompt must produce code after :=, forbids sorry, and may return an empty string if it judges a theorem unprovable (sections 3.2–3.3, PDF pp. 3–4). The separation is intended to avoid duplicate statements and allocate multiple proof attempts to a fixed statement. The authors summarize the design: “By separating the conjecturing and proving phases, we avoid the generation of identical theorems and encourage proving more difficult theorems.” (section 3.1, PDF p. 3).

Inference: a Verus implementation would represent conjectures as candidate spec fn properties or ensures contracts and send each candidate to Verus, retaining only candidates whose proof functions verify. A Rust orchestration process can keep the candidate library and invoke Verus repeatedly; it must not put sorry-like axioms into the accepted library. Verus’s executable function, requires/ensures contracts, loop invariants, and proof fn lemmas are the relevant constructs. Lean’s exact? novelty check has no direct Verus equivalent, so novelty would need normalized signatures, declaration-name checks, or an explicit equivalence/specification query (inference).

Evidence: in 20 runs with GPT-o3, CPL generated 106 theorems on average and discovered the target theorem in 5/20 runs; the simple loop (SL) generated 328 on average and discovered it in 0/20. Fisher’s exact test gave p = 0.024 (section 5.2, PDF p. 7). The target was the intersection theorem for anonymous alpha-open sets, selected because it is the difficult part of showing alpha-open sets form a topology. The denominator is 20 independent libraries per framework, with a 14,000,000-token API budget per run (section 5.1, PDF p. 7). The comparison does not show that CPL always discovers more theorems: SL produced about three times as many accepted theorems, but they were mostly easier.

technique: retain verified proofs as in-context strategy examples

Use this when a prover can produce valid code for some statements but fails on a harder statement. CPL includes the entire previously generated library in the prover context (section 3.1, PDF p. 3). The prover therefore sees theorem statements and their checked proof terms before the target statement. The paper describes the intended effect as: “the proving ability of LLMs can be improved by in-context learning, when the verified proofs generated by LLMs themselves before the statement of a target theorem is provided are given as context.” (section 1, PDF p. 2).

To apply it, preserve each verified pair, format it as ordinary Lean declarations, place those declarations before the target, and return Lean’s error message after every failed attempt. Do not treat an LLM assertion as evidence; Lean acceptance is the filter. In a targeted re-proof experiment, the authors replayed every CPL theorem with either its prior generated library or only the seed definitions. With context, 2,106/2,123 theorems (99%) were reproved; without context, 1,935/2,123 (91%). These are denominators over all 2,123 CPL theorems in that re-proof test, not the 20 discovery runs (section 5.3.2, PDF p. 9). McNemar’s test reported p = 4 × 10^-35.

For the target theorem, five generated contexts were each tested 16 times. Contextual re-proof succeeded 7 times in total, while the no-context setting succeeded 0 times (section 5.3.3, PDF p. 10); the paper says the average library length before discovery was 49 theorems. The generated target proof did not use generated theorems as lemmas, so the result is evidence that examples teach proof strategy rather than merely supply a direct lemma.

Inference: in Verus, retain verified proof fn lemmas and their contracts as prompt examples, then ask a model to write a new proof fn or strengthen a function’s ensures. Re-run Verus after every attempt and feed diagnostics back. Verus’s proof terms can be erased at runtime, so only verified examples should enter the prompt corpus; this does not make the specification itself trustworthy (inference).

technique: stratified search for hard statements

The paper models SL’s accepted-theorem probability as proportional to s(T) r(T), where s(T) is statement-generation probability and r(T) is proof success probability. CPL’s probability is proportional to s(T)(1-(1-r(T))^N) for N proof attempts (section 4, PDF pp. 5–6). Increasing N reduces the suppression of statements that are meaningful but hard for the prover. The authors derive expected proof-trial costs and show E_SL <= E_CPL, explaining why CPL yields fewer total theorems while shifting its accepted distribution toward low-r statements. This is a sampling argument under a simplified model that ignores context effects; it is not a measured universal law.

Inference: a Verus search controller can assign a fixed retry budget per candidate contract and keep candidates after failed proofs, instead of sampling a fresh contract-proof pair each time. Retry budgets should be observable because larger N increases verification cost. The controller can rank candidates by semantic novelty and proof difficulty, but difficulty estimates beyond Verus diagnostics are an engineering extension (inference).

what is proved, measured, and trusted

Lean kernel checking proves the accepted Lean declarations under Mathlib and the supplied definitions. The experiments measure discovery counts, re-proof rates, proof lengths, and statistical tests; they do not prove that an LLM’s conjecture is mathematically useful beyond Lean’s formal statement. The setup trusts Lean, Mathlib, the Lean Server’s error feedback, model/API behavior, and the seed definitions. It also trusts that the target’s formalization captures the intended topology fact. The paper’s natural-language control experiment exposes model unreliability: GPT-4o called the target false 10 times and produced incorrect proofs 6 times, while GPT-o3 always judged it false in the reported trials (section 5.3.3, PDF p. 10). These counts are model-specific judgments, not kernel-checked proofs.

Limitations include a small domain (three topology notions), one model family (GPT-o3 for the main comparison), finite 16-attempt budgets, and API-token budgets. The paper notes that the selected propositions were relatively natural to conjecture and calls for harder domains (section 6, PDF p. 10). Inference: the threat to VeruLaw is moderate for proof-search orchestration: CPL supplies a concrete pattern for harvesting verified lemmas and retrying contracts, but it does not solve Rust translation, specification adequacy, unsafe APIs, or dependency trust. Reusing the architecture without Verus-specific novelty and contract checks would therefore leave major product risks unchanged (inference).

techniques for the catalog

  • conjecture-proving separation — generate Lean statements first, then spend a bounded proof budget on each surviving statement
  • verified-proof context — feed only kernel-checked prior statements and proofs to the next prover prompt
  • Lean novelty filtering — use exact? against Mathlib and the generated library before proof search
  • verifier-feedback retries — return Lean diagnostics to the prover for up to a fixed attempt limit
  • stratified hard-theorem sampling — use multiple proof attempts so acceptance is less biased toward statements with easy proofs Checked 2026-10-15 against paper kasaura2025discovering: full comparison completed; metadata and unsupported claims reviewed; experiments not reproduced

Last edited: