Lean premise retrieval research system

ProofAtlas

A midterm report on theorem-neighborhood evidence for Lean premise retrieval

ProofAtlas builds a theorem-neighborhood retrieval pipeline, evaluates LLM-enriched theorem profiles as a source of premise evidence, and exposes interpretable retrieval evidence for inspection.

Executive Summary

Midterm progress is best read as a capability build-out first, then a hard challenge benchmark. ProofAtlas now has theorem-neighborhood retrieval infrastructure, interpretable retrieval evidence views, and an initial proof-state premise retrieval result.

Built

Theorem-Neighborhood Pipeline

  • theorem-disjoint Lean proof split
  • 127,561 train-side premise pool
  • LLM theorem enrichment
  • weighted RRF fusion
Validated

Mechanistic Retrieval Signal

  • LLM-enriched theorem profiles improve theorem-neighbor premise evidence
  • theorem neighborhoods expose reusable premise suggestions
  • strategy and difficulty facets are inspectable
Challenged

Hard Premise Retrieval

  • 3,053 held-out proof states
  • 7,054 gold premise edges
  • Top-100 retrieval from 127,561 train-side premises
  • candidate recall roughly doubles over dense retrieval
Identified

Next Bottleneck

  • top-rank precision remains limited
  • learned reranking is the next system step
  • downstream prover evaluation is still needed

Dataset & Evaluation Scope

Task: given a held-out proof state, retrieve useful premises from 127,561 train-side candidate premises.

Split Theorems Proof states Premises Positive edges
train 8000 23723 127561 54897
test 1000 3053 38332 7054

System Pipeline

The system has two retrieval evidence paths and one explanation layer. LLM enrichment turns theorem metadata plus proof-state context into profiles for retrieving similar train theorems. Those neighbors produce premise evidence for the challenge fusion, and they also feed an interpretable evidence view for inspection.

LLM enrichment is retrieval text only; it does not use gold premise labels or proof scripts as target answers.

The challenge evaluation fuses proof-state evidence with neighbor-derived premise evidence by weighted RRF. BGE fusion is reported separately as an auxiliary recall-maximizing variant.

ProofAtlas retrieval pipeline graph LeanRank data is split into a proof-state retrieval path and an LLM theorem-neighborhood path. The theorem-neighborhood path is evaluated as a mechanism check, also feeds an interpretable evidence view, and then contributes neighbor-derived premise evidence to weighted RRF fusion. LeanRank processed data theorem-disjoint train / test split Proof-state evidence path Capability 1: theorem-neighborhood mechanism test proof state goal + hypotheses dense + lexical retrieval proof-state expansion proof-state evidence theorem metadata + state context goals / hypotheses / symbols LLM theorem enrichment semantic / strategy / difficulty profile similar train theorems neighbor premise evidence neighbor-derived premise evidence mechanism eval: Recall@100 not theorem-name matching Capability 2 evidence view neighbors / premises strategy / difficulty weighted RRF fusion weighted_rrf_llm_theorem_tuned Challenge: Top-100 ranked premise candidates Challenge evaluation held-out proof-state positives Recall@100 / nDCG@10 LeanRank processed data theorem-disjoint train / test split proof-state evidence dense + lexical + expansion theorem metadata + state goals / hypotheses / symbols LLM theorem enrichment semantic / strategy / difficulty similar train theorems neighbor premise evidence Capability 1 mechanism eval neighbor-premise Recall@100 not theorem-name matching Capability 2 evidence view neighbors + premise suggestions strategy + difficulty signals proof-state evidence + neighbor-derived evidence for challenge fusion weighted RRF fusion weighted_rrf_llm_theorem_tuned Challenge Top-100 candidates held-out proof-state positives Recall@100 / nDCG@10

Terms Used Here

Short definitions for the main abbreviations and proof-retrieval terms used below.

Lean
A theorem prover and proof assistant used to formalize mathematics.
LeanRank
The processed Lean proof dataset source used by this experiment.
Proof state
The current goal, hypotheses, and local context at a point in a Lean proof.
Premise
A theorem, lemma, definition, or fact that may help prove a proof state.
Gold premise edge
A held-out labeled link between a proof state and a premise used in the reference proof.
Theorem-disjoint split
A train/test split where test theorems do not appear in training.
Train-side premise pool
The candidate premises available for retrieval from the training side.
Theorem neighborhood
Similar train theorems retrieved for a held-out theorem or proof state.
LLM
Large language model; here it generates retrieval text, not evaluation labels.
TF-IDF
Term frequency-inverse document frequency, a lexical text retrieval representation.
BGE
An external pretrained embedding model used as an auxiliary variant; the report records the exact model name.
Dense retrieval
Nearest-neighbor retrieval using vector embeddings.
Lexical retrieval
Retrieval based on token overlap or weighted text features such as TF-IDF.
RRF
Reciprocal-rank fusion, a method for combining ranked candidate lists.
Recall@100
Whether gold premises appear within the top 100 retrieved candidates.
R@k
Short chart label for Recall@k, such as R@10 or R@100.
Covered Recall
Recall over gold premises that are present in the retrievable train-side pool.
All-positive Recall
Recall over all held-out positive premise edges, including non-retrievable positives.
MAP
Mean average precision, a ranking-quality metric over the retrieved list.
nDCG@10
Normalized discounted cumulative gain at rank 10, a top-rank quality metric.
Challenge evaluation
Proof-state to premise retrieval from the full train-side candidate pool.
Retrieval evidence view
An explanation layer showing theorem neighbors, premise suggestions, and strategy facets behind retrieved candidates.

Capability 1: LLM-Enriched Theorem Neighborhood Retrieval

This capability answers: can ProofAtlas retrieve useful similar theorems? Given a held-out theorem profile, the system uses LLM-enriched theorem text to find similar train-side theorems, then checks whether premises from those neighbors are useful evidence. The LLM-enriched TF-IDF profile improves neighbor-premise Recall@100 from 0.3185 to 0.3774 and nDCG@10 from 0.1499 to 0.1717.

Evaluation expands retrieved theorem neighbors into the premises used in their proof states, then measures whether held-out gold premises appear in the resulting neighbor-derived premise candidates. Neighbor-premise Recall@100 is a premise-evidence metric, not direct theorem-name matching.

Theorem-Neighborhood Retrieval Comparison

0 0.20 0.40 0.1985 0.3279 0.3774 0.1257 0.1717 R@10 R@50 R@100 MAP nDCG@10 Baseline profile LLM TF-IDF profile LLM BGE profile

LLM-enriched TF-IDF theorem profiles produce the strongest theorem-neighborhood premise retrieval.

Capability 2: Interpretable Retrieval Evidence

This capability answers: what evidence did those similar theorems provide? It is the explanation layer for the retrieval system, not a separate performance benchmark. For a query theorem, ProofAtlas exposes similar train theorems, neighbor-derived premise suggestions, strategy facets, difficulty signals, and retrieval methods that contributed evidence. The example illustrates visible evidence for inspection, not an aggregate claim.

Proof Strategy Facet Taxonomy

ProofAtlas uses 15 broad strategy facets as interpretable labels. They summarize recurring proof patterns; they are not final tactic predictions.

algebraic_computation
Ring, field, arithmetic, and normalization-style algebraic calculation.
case_analysis
Splitting the proof into constructors, alternatives, or conditional cases.
category_morphism_reasoning
Reasoning about categorical morphisms, composition, identities, and commutative diagrams.
contradiction_negation
Using negation, contradiction, impossible hypotheses, or proof by contradiction.
existential_construction
Building witnesses for existential goals or packaging data into structures.
extensionality
Proving equality by showing pointwise, componentwise, or structural equality.
induction_recursion
Using induction, recursion, or structural decomposition over inductive objects.
measure_ae_reasoning
Measure-theoretic reasoning with almost-everywhere statements and measurable sets.
order_inequality_reasoning
Manipulating inequalities, monotonicity, bounds, lattice/order facts, or comparisons.
rewrite_transport
Rewriting goals across equalities, equivalences, casts, coercions, or transported structures.
set_membership_reasoning
Reasoning about set membership, subsets, intersections, unions, images, and preimages.
simplification_normalization
Simplifying definitions, canonical forms, coercions, and routine goals.
theorem_application
Solving a goal mainly by applying a known lemma, theorem, or hypothesis.
topology_filter_limit
Reasoning about continuity, filters, neighborhoods, convergence, and limits.
typeclass_instance_resolution
Using or constructing typeclass instances and inherited algebraic/order/topological structure.
Domain: AlgebraicGeometry AlgebraicGeometry. HasRingHomProperty.stalkwise stalkwise_Spec_map_iff locally_of_iff RingHom.toMorphismProperty Localization.Away rewrite transport localization reasoning Difficulty: hard difficulty bucket retrieved by weighted RRF proof states local goals + hypotheses

Top Theorem Neighbors

  • AlgebraicGeometry.stalkwise_Spec_map_iff
  • AlgebraicGeometry.HasRingHomProperty.locally_of_iff
  • RingHom.locally_stableUnderComposition
  • RingHom.RespectsIso.arrow_mk_iso_iff

Premise Suggestions

  • RingHom.toMorphismProperty
  • Localization.Away
  • algebraMap
  • CategoryTheory.MorphismProperty.RespectsIso

Strategy Facets

  • rewrite_transport
  • algebraic_computation
  • case_analysis
  • set_membership_reasoning

Example Retrieval Neighborhoods

These qualitative views list concrete evidence exposed by ProofAtlas for two held-out theorems. They are examples, not aggregate performance claims.

AlgebraicGeometry.HasRingHomProperty.stalkwise

Domain: AlgebraicGeometry | Difficulty: hard | Theme: stalkwise/localization criteria

query theorem HasRingHomProperty.stalkwise 10 similar theorems 10 premise suggestions 8 strategy facets hard difficulty bucket
Neighbors
  • AlgebraicGeometry.stalkwise_Spec_map_iff
  • AlgebraicGeometry.HasRingHomProperty.locally_of_iff
  • RingHom.locally_stableUnderComposition
Premises
  • RingHom.toMorphismProperty
  • Localization.Away
  • algebraMap

Emphasizes scheme-local reasoning, localization, prime spectra, and morphism-property transport.

Algebra.Presentation.aeval_val_relation

Domain: RingTheory | Difficulty: hard | Theme: generators and relations

query theorem Algebra.Presentation.aeval_val_relation 10 similar theorems 10 premise suggestions 8 strategy facets hard difficulty bucket
Neighbors
  • Algebra.Generators.aeval_val_eq_zero
  • Algebra.Presentation.fg_ker
  • PowerBasis.mem_span_pow
Premises
  • Algebra.Generators.algebraMap_apply
  • WithBot.coe_lt_coe
  • Set.Finite.toFinset

Emphasizes polynomial evaluation, ideals, span membership, and relations vanishing under evaluation.

Challenge Evaluation: Proof-State -> Premise Retrieval

This is the hard benchmark: retrieve useful train-side premises for 3,053 held-out proof states from a 127,561-premise pool. The challenge result shows that the pipeline improves top-100 candidate generation, while top-rank precision remains the next-stage bottleneck.

Covered Recall@100 0.2362 -> 0.4746 +0.2384
All-positive Recall@100 0.1851 -> 0.4074 +0.2223
Covered Recall@50 0.1961 -> 0.3894 +0.1933
nDCG@10 0.0697 -> 0.1236 +0.0539

Dense vs Primary Method

0 0.25 0.50 0.2362 0.4746 0.1851 0.4074 0.0697 0.1236 Cov R@100 All-pos R@100 MAP nDCG@10 Dense baseline Primary method

Primary method: weighted_rrf_llm_theorem_tuned. MAP remains in the full report and ablation chart.

Ablation Progression

0 0.25 0.50 0.236 0.389 0.462 0.475 0.481 dense lexical d+l union ps tuned thm LLM thm BGE aux Covered Recall@100 MAP

Most gain over dense comes from multi-source fusion and proof-state expansion; theorem-neighborhood evidence adds a further incremental lift.

The held-out result suggests theorem-theorem retrieval can provide useful auxiliary premise evidence when fused with proof-state retrieval signals. The next bottleneck is top-rank precision, where a learned reranker over the fused candidate pool is the natural follow-up.

Next Phase

Work after the midterm checkpoint focuses on ranking quality and downstream validation.

  • learned reranker
  • prover-in-the-loop evaluation
  • statement-only / no-symbol leakage ablations
  • larger theorem-neighborhood evaluation
  • improve top-10 ranking quality