LeanDojo Proof Geometry Experiments

An empirical study of how theorem statements, human-written Lean proofs, and proof-generation behavior relate across LeanDojo Benchmark 4.

The repository follows a single research arc:

1. separate proof procedure (tactic style) from mathematical subject (explicit premise vocabulary);
2. compare statement and proof representations in learned semantic spaces;
3. test whether nearby statements have nearby recorded proofs; and
4. intervene by retrieving examples before generation and checking every candidate with Lean.

Explore the project site · Open the 3-D proof-space viewer · Read the papers · Read the experiment index

Results at a glance

• At 10,000 proofs, tactic-style and premise-domain topics have only weak alignment: adjusted mutual information (AMI) is 0.0153 and Cramér's V is 0.102.
• Statement-only and proof-only semantic clusters also differ globally (AMI 0.0804), but local geometry is informative: at k = 10, statement neighbors' proofs are 0.0696 cosine points closer than a context-matched random baseline.
• In the paired 100-target generation pilot, semantic retrieval reached 24% pass@3, versus 21% for BM25, 16% with no retrieval, and 14% with random examples. The pilot supports useful retrieval, but does not establish that semantic retrieval is better than BM25.

These are descriptive and pilot-scale findings, not claims that proof spaces have a canonical number of clusters or that theorem statements determine proofs. The full reports retain uncertainty estimates, controls, and caveats.

Papers and reports

• Textures of Modern Formal Mathematics — tactic style, premise vocabulary, and the separation between procedure and mathematical domain.
• What Statements Know, What Proofs Do — statement, proof, and joint embedding geometries across 10,000 theorem–proof pairs.
• Nearby Examples, New Proofs — the paired retrieval-guided Lean proof-generation pilot and kernel-verified outcomes.
• Proof Space Has More Than One Geometry — a synthesis connecting the experiments to proof theory, formal-library networks, representation learning, and retrieval-guided proving.
• The Infrastructure–Isolation Principle — an empirical principle relating dependency reliance, semantic isolation, and proof complexity, with a rank-sign law and one-factor diagnostic.

Mathematical sketch

For a proof $t$ with tactic-head sequence $(h_1,\ldots,h_L)$, the style view retains tactic unigrams and adjacent bigrams:

$$ \Phi_{\mathrm{style}}(t) ={\mathtt{TAC}(h_i)}_{i=1}^{L} \uplus {\mathtt{BIGRAM}(h_i,h_{i+1})}_{i=1}^{L-1}. $$

If $P(t)$ is the set of explicitly annotated premises and $\nu(p)$ is the top-level namespace of premise $p$, the domain view is

$$ \Phi_{\mathrm{domain}}(t) ={\mathtt{PREM}(p),\mathtt{NS}(\nu(p)):p\in P(t)}. $$

For each view $v\in{\mathrm{style},\mathrm{domain}}$, the feature matrix is TF–IDF weighted and approximated by nonnegative matrix factorization:

$$ X_v=\mathrm{TFIDF}(\Phi_v) \approx W_vH_v, \qquad W_v,H_v\geq0. $$

The row-normalized proof mixture is

$$ \theta_{ik}^{(v)} =\frac{(W_v)_{ik}}{\sum_j(W_v)_{ij}}. $$

Let $s_i$ and $p_i$ be the normalized statement and proof embeddings for theorem $i$. Their exact top $k$ neighborhoods are

$$ S_i(k)=\mathrm{TopK}_{j\neq i}\cos(s_i,s_j), \qquad P_i(k)=\mathrm{TopK}_{j\neq i}\cos(p_i,p_j). $$

The local transfer statistic compares proof similarity along statement neighbors with a context-matched random neighborhood $R_i(k)$:

$$ \Delta_k =\mathbb{E}_{j\in S_i(k)}[\cos(p_i,p_j)] -\mathbb{E}_{j\in R_i(k)}[\cos(p_i,p_j)]. $$

At $k=10$, the observed value is $\Delta_{10}=0.6727-0.6030=0.0696$. For generation condition $c$, kernel-verified success is

$$ \mathrm{pass}_{k}(i,c) =\mathbb{1}!\left[ \exists j\leq k:\mathrm{LeanAccept}(p_{ij}^{(c)}) \right]. $$

Repository guide

Path	Contents
experiments/	Frozen designs, scripts, inputs, outputs, and results for five completed experiments
notes/	Four compact LaTeX/PDF research notes and their figure-generation code
app/	Dependency-free interactive 3-D viewer for the original 1,940-proof analysis
pipeline.py	Shared style/domain topic pipeline for the 1,940- and 10,000-proof profiles
scripts/	Cross-view analysis and small artifact/reporting utilities
FINDINGS.md	Full write-up of the original style/domain experiment
out/	Historical artifacts consumed by the original viewer and reporting utilities

Large arrays and raw model/verifier outputs are checked in intentionally so the published analyses can be inspected without rerunning paid services. The LeanDojo benchmark itself is not redistributed; data/ is local and ignored.

Quick start

Python 3.13 was used for the recorded local runs. Create an environment and install the pinned analysis dependencies:

python -m venv .venv
.\.venv\Scripts\Activate.ps1
python -m pip install -r requirements.txt

Place LeanDojo Benchmark 4 at:

data/leandojo_benchmark_4/leandojo_benchmark_4/

Then reproduce either tactic-style/domain profile from the repository root:

python pipeline.py --profile small-1940
python pipeline.py --profile aws-10000

The larger semantic and generation studies have additional AWS, model-access, or Lean/Mathlib requirements. Their local READMEs contain exact commands and frozen configuration:

• semantic-embeddings-10000
• semantic-neighborhood-transfer-10000
• retrieval-guided-proof-generation-100

Explore without installing anything

Open app/index.html directly in a browser. Its data is embedded through app/data.js, so the viewer works from file:// and has no CDN or server dependency. It supports theorem/file search, PCA and t-SNE layouts, proof-length sizing, and style/domain coloring.

The repository root index.html is the GitHub Pages landing page. It can be previewed locally by opening the file; MathJax is loaded from jsDelivr for the small amount of typeset mathematics.

Reproducibility boundaries

• Randomized local analyses use recorded seed 0 unless an experiment says otherwise.
• Semantic embeddings and raw generation responses are retained with checksums and provenance metadata.
• Bedrock generation at temperature 0.4 is not bit-for-bit reproducible because the API did not expose a sampling seed.
• Lean acceptance was checked against the pinned historical Mathlib context; setup instructions live with the generation experiment.
• Generated PDFs are checked in alongside their sources for convenient review.

Project status

All five documented experiments and four notes are complete. The natural next step is a larger paired comparison of semantic retrieval, BM25, and no retrieval; that run has not been performed in this repository.

License

This repository uses a split license:

• Original source code is licensed under the MIT License.
• Original reports, research prose, figures, LaTeX source, rendered PDFs, and website content are licensed under Creative Commons Attribution 4.0.
• LeanDojo/Mathlib-derived material, retained model or embedding outputs, and other third-party content are not relicensed; see THIRD_PARTY.md.

Copyright © 2026 Jonathan R. Landers.