Lean theorem proving · empirical study

What travels between a theorem and its proof?

Jonathan R. Landers

A sequence of experiments asks how much structure survives the map \(\text{theorem} \longleftrightarrow \text{proof}\), then tests that structure in kernel-verified Lean generation.

Explore proof space Read the overview

5 completed experiments
Kernel-verified pilot
Artifacts included

Statement space Proof space

10,000Theorem–proof pairs

+0.0696Local proof-cosine lift

24%Semantic retrieval pass@3

Represent\(X_v=\operatorname{TFIDF}(\Phi_v)\)

Factor\(X_v\approx W_vH_v,\quad W_v,H_v\geq0\)

Mix\(\theta_{ik}=\dfrac{W_{ik}}{\sum_j W_{ij}}\)

Research arc

From description to intervention

Each experiment tightens the question: first distinguish structures, then measure their local relationship, then test whether the relationship is useful.

01 / Separate

Procedure is not subject

Tactic unigrams and bigrams model proof style; explicit premises and namespaces model mathematical domain.

\(\Phi_{\mathrm{style}} \neq \Phi_{\mathrm{domain}}\)

Style ↔ domain AMI 0.0153

02 / Compare

Global mismatch, local signal

Statement and proof clusters differ, yet nearby statements have measurably more-similar recorded proofs.

\(\Delta_{10}=0.6727-0.6030=0.0696\)

Top-10 proof cosine +0.0696

03 / Test

Retrieve, generate, verify

Four retrieval conditions share the same held-out targets; every candidate is checked in its pinned Lean context.

\(\operatorname{pass@}k=\mathbb{1}[\exists j\!\leq\!k:\operatorname{Lean}(p_j)]\)

Semantic 24% · BM25 21%

Interactive artifact

Orbit the original proof space

Explore 1,940 tactic proofs in a dependency-free 3-D viewer. Switch between style and domain coloring, compare PCA with t-SNE, search theorem names and files, and inspect proof scripts.

\(X_{\mathrm{style}}\xrightarrow{\mathrm{SVD}_{64}}Z\xrightarrow{\mathrm{PCA}_3\;\mathrm{or}\;t\text{-}\mathrm{SNE}_3}\mathbb{R}^3\)

Launch viewer Read findings

Experiment index

Five completed studies

Frozen settings, machine-readable artifacts, exact prompts, verifier output, analysis code, and full interpretations live together.

Statement neighbors\(S_i(k)=\operatorname{TopK}_{j\ne i}\cos(s_i,s_j)\)

Proof neighbors\(P_i(k)=\operatorname{TopK}_{j\ne i}\cos(p_i,p_j)\)

Cross-view overlap\(O_i(k)=\dfrac{|S_i(k)\cap P_i(k)|}{k}\)

Experiment	Scale	Question	Status
Original topic study	1,940 proofs	Which tactic styles and premise domains recur?	Complete
Large-sample replication	10,000 proofs	Does weak style/domain alignment survive scale?	Complete
Semantic embeddings	10,000 pairs	How do statement, proof, and joint spaces align?	Complete
Neighborhood transfer	10,000 pairs	Do nearby statements have nearby recorded proofs?	Complete
Generation pilot	100 targets	Does relevant retrieval improve verified generation?	Complete

Research notes

Compact paper-style reports

Five standalone PDFs present the experiment sequence and connect it to proof theory, formal-library networks, representation learning, retrieval-guided theorem proving, and the infrastructure–isolation pattern.

Normalized mixture entropy\(E_i=-\dfrac{\sum_k\theta_{ik}\log\theta_{ik}}{\log K},\qquad 0\leq E_i\leq1\)

Cosine similarity\(\cos(x,y)=\dfrac{x^{\mathsf T}y}{\lVert x\rVert_2\lVert y\rVert_2}\)

Note 01 · PDFProof style and mathematical domainThe original two-view topic analysis.Open report → Note 02 · PDFSemantic theorem/proof embeddingsGlobal clusters and cross-view alignment.Open report → Note 03 · PDFRetrieval-guided generationPaired conditions and Lean-verified outcomes.Open report → Note 04 · PDFProof geometry in contextA synthesis with adjacent research traditions.Open report → Note 05 · PDFThe Infrastructure–Isolation PrincipleReliance, semantic neighborhoods, and proof complexity.Open report →