Summary (Overview)

• This paper introduces MathKG, a semantic knowledge graph of 364 verified Mathlib theorems and definitions connected by 9,434 typed edges in eight relational categories (e.g., generalizes, analogous-to, cross-domain-bridge), built via an LLM-based relation extraction pipeline anchored to verified Mathlib declarations. It also presents MathAgent, a four-agent LLM system (Explorer, Conjecturer, Prover, Integrator) coordinated by an Orchestrator, that uses MathKG as shared memory for theorem proving in Lean 4.

• The authors run a controlled ablation across four augmentation modes (no external context, knowledge-graph context, Mathlib library retrieval, both combined)and five models: general-purpose Qwen3-8B/32B, Lean-specialized Goedel-Prover-V2-8B/32B, and proprietary Claude Sonnet 4.6, evaluated on miniF2F (and PutnamBench, MathOlympiadBench for Sonnet).

• Finding 1 (Specialization dominates augmentation): Lean fine-tuning adds 33–38 percentage points of solve rate in every augmentation mode, and a specialized 8B model beats a 4× larger general model by 29–35 points; no augmentation mode improves solve rate by more than 3 points, showing external knowledge does not substitute for competence in the weights.

• Finding 2 (Augmentation is capability-conditioned): Knowledge-graph context helps small models (e.g., Goedel-8B: +14 problems) but hurts large ones (e.g., Qwen3-32B: −14; Sonnet: −7); Mathlib retrieval never helps on aggregate ( −6 to 0).

• Finding 3 (Complementarity): The augmentation modes solve different problems, so an oracle that selects the best mode per problem solves 6% to 58% more problems than the unaugmented prover, with gains growing on harder benchmarks (+32% on PutnamBench). This motivates adaptive strategies that select augmentation by model capability and problem.

Introduction and Theoretical Foundation

Large language models (LLMs) are becoming capable theorem provers, especially when combined with search and formal verification in Lean 4, producing IMO-level proofs. Specialized open provers like Goedel-Prover-V2 are fine-tuned on large corpora of machine-verified Lean proofs; everything they know about mathematics is stored in their weights. Mathematicians, however, draw on a shared semantic web of the field: analogies across subfields, generalizations, and cross-domain bridges, which remain implicit in formal libraries like Mathlib (which encode only syntactic dependencies). The paper asks: if we make this semantic layer explicit and hand it to an LLM prover at inference time, does it prove more theorems? And for which models, and does the answer vary by problem?

The theoretical foundation rests on the distinction between parametric knowledge (stored in model weights via fine-tuning)and non-parametric knowledge (supplied at inference time via retrieval or knowledge graphs). The authors hypothesize that structured knowledge might help most when the model’s parametric knowledge is weakest, echoing findings in retrieval-augmented question answering (Mallen et al., 2023).

The paper introduces MathKG, a directed graph $G = (V, E)$ where:

• Nodes are 364 Mathlib-verified theorems and definitions across seven domains (number theory, combinatorics, algebra, abstract algebra, linear algebra, analysis, Euclidean geometry), each with a natural-language statement, keywords, and its Mathlib declaration name.

• Edges are typed semantic relations $(A, B, r, c, \rho)$ with relation type $r \in R$, confidence $c \in [0,1]$, and justification $\rho$; the eight edge types are: prerequisite, generalizes, specializes, equivalent-to, applied-in, analogous-to, cross-domain-bridge, and instance-of.

Methodology

MathKG Construction: The authors asked Claude Opus 4.7, Gemini 3.1 Pro, and GPT-5.4 for fundamental theorems and definitions in seven domains, cross-checked the lists, and kept entries with formalizations in Mathlib, yielding 229 theorems and 135 definitions. Relation extraction was performed by prompting Claude Sonnet 4.6 for each of the 132,132 directed pairs of nodes, with a prompt that included the ontology, few-shot examples, and type restrictions. Edges with confidence below $\tau = 0.75$ were discarded; post-processing enforced node-type restrictions (e.g., generalizes requires both endpoints to be theorems)and removed contradictory cycles. The final graph had 8,026 LLM-inferred edges plus 1,408 auto-inverse edges = 9,434 total.

MathAgent Architecture: The system uses four LLM agents sharing MathKG as persistent memory:

• Explorer: In targeted problem-solving mode, performs a two-layer search: (1) MathKG semantic search (domain pre-filter, LLM seed selection of $s=5$ seeds, one-hop edge walk, context assembly)and (2) Mathlib declaration search(prefix-matching extracted Lean identifiers against the declaration database, scoring, ranking, type-signature enrichment).
• Prover: Attempts a complete Lean 4 proof with error-guided refinement: initial generation with context, Lean verification, and up to $K=32$ attempts feeding back previous code and error messages. .
• Conjecturer and Integrator: Used in open-ended exploration mode(implemented but not evaluated in this paper).

Ablation Setup: Four augmentation modes correspond to lines of Algorithm 1: prover_only (no context), with_kg (MathKG semantic context), with_mathlib (Mathlib retrieval context), and full_system (both). Five models were evaluated at pass@32 on miniF2F (488 problems); the proprietary model additionally on PutnamBench(672)and MathOlympiadBench(360). The four open-weight models formed a matched 2×2: Qwen3-8B/32B (general) vs. Goedel-Prover-V2-8B/32B (Lean-specialized, fine-tuned from the Qwen3 bases).

. All LLM calls in a run, including the Explorer’s scoring, used that run’s model, so results measure the end-to-end system.

Empirical Validation / Results

Table 2: Cross-model pass@32 solve rates on miniF2F (488 problems). Best mode in bold.

Finding 1 — Specialization dominates: Goedel-8B solves 205/488 (42.0%) versus 62/488 (12.7%) for Qwen3-32B without context, a 29-point gap despite being four times smaller. Within matched pairs, specialization adds 35.2 points at 8B and 35.9 points at 32B in prover_only. No augmentation mode improves solve rate by more than 3 points.

.

Finding 2 — Capability-conditioned augmentation:

Table 3: Solve-count deltas on miniF2F (positive: augmented mode solves more; ∗: p < .05).

KG augmentation helps the specialized small model most (Goedel-8B, +14), helps the weak general model marginally (Qwen3-8B, +2), is roughly neutral on the large specialized model (Goedel-32B, −3), and hurts the large general model (Qwen3-32B, −14)and the proprietary model (Sonnet, −7). Mathlib retrieval never helps on aggregate. Context overflow in Goedel-32B (10 problems in with_kg, 28 in full_system) partially explains the negative deltas; excluding them, with_kg becomes +1 over prover_only.

Finding 3 — Complementarity:

Table 4: Complementarity on miniF2F (488 problems). Oracle: union of problems solved by any of the four modes.

Relative gains over prover_only are: +58% for Qwen3-8B, +29% for Qwen3-32B, +18% for Goedel-8B, +12% for Goedel-32B, and +6% for Sonnet. The oracle beats the no-context baseline for every model, even Sonnet, where no fixed mode improves the aggregate by more than one problem. This complementarity strengthens on harder benchmarks: for Sonnet, the oracle exceeds prover_only by +6% on miniF2F, +28% on MathOlympiadBench, and +32% on PutnamBench.

Table 8 (Sonnet full ablation): Oracle exceeds prover_only by +6% to +32%, most on PutnamBench.

Across the three benchmarks, augmentation recovers 45 problems that prover_only misses and loses 13, a roughly 3:1 ratio.

Theoretical and Practical Implications

• Theoretical implication: The results challenge the assumption that external structured knowledge can substitute for model competence. Instead, they suggest a capability-conditioned view: augmentation helps most when the model’s parametric knowledge is weakest (small models)and can hurt when the model already knows the answer(large models). This parallels findings in retrieval-augmented LLMs generally.

• Practical implication: The complementarity effect is the most actionable finding: since different augmentation modes solve different problems, an adaptive system that selects the augmentation mode per problem—based on model capability and problem difficulty—could yield substantial gains (up to +58% relative for weak models, +32% on PutnamBench for Sonnet),, without changing the underlying prover. This motivates future work on learned or heuristic selectors rather than uniform application of any single augmentation strategy. .

• Design implication for MathKG: The graph’s value lies in its typed semantic edges (e.g., cross-domain-bridge, analogous-to) that provide reasoning for connections, unlike dependency-only graphs. The authors note the graph is deliberately small(a fundamentals-only core) to keep exhaustive pairwise extraction feasible and avoid burying fundamentals under specialized lemmas; specialized lemmas are left to Mathlib retrieval, which proved uniformly unhelpful in this setup, suggesting that semantic context matters more than raw formal signatures for weaker models.

Conclusion

The paper set out to measure whether, and when, structured mathematical knowledge helps LLMs prove theorems in Lean 4. Three lessons emerge:

1. Specialization dominates augmentation: What a model knows in its weights matters far more than what is supplied at inference time; Lean fine-tuning is worth 33–38 percentage points of solve rate, while no augmentation mode improves solve rate by more than 3 points. Structured knowledge is no substitute for specialization.
2. Augmentation is capability-conditioned: Knowledge-graph context lifts small provers but hurts larger ones, with the specialized model gaining more relative to its general base at every scale; Mathlib retrieval never helps on aggregate. .
3. The aggregates hide complementarity: The augmentation modes solve different problems, so a per-problem selector would solve 6–58% more than the unaugmented prover, a margin that widens on harder benchmarks. The value of augmentation is real but latent, unlocked by selection rather than by uniform application.

Future directions include developing adaptive proving strategies that choose augmentation by model capability and problem, and extending the evaluation to more models and benchmarks. The authors release all code, graph data, and evaluation infrastructure for the AI-for-math community at https://github.com/sarehnabi/mathagent.