Research and publications.
A formal verification of Wolstenholme’s theorem — (2p choose p) ≡ 2 (mod p³) for prime p ≥ 5 — in Lean 4 with Mathlib. Nine lemmas across approximately 800 lines of Lean, with zero sorry declarations. To our knowledge, the first formal verification of Wolstenholme’s theorem in Lean 4. Discovered through a collaboration between a relational analogy engine for theorem proving and human-directed formalization.
Alexandre Linhares · April 2026
Method introduction: tactic-usage distributions extracted across 27 Mathlib areas (217,133 proof states), z-scores identify tactics heavily used in a source but rare in a target, matched via GPU-accelerated NP-hard analogy. 4 Lean-verified new proofs from 10 attempts (40%). Key finding: tactic schemas decompose into head (domain-gated) and modifier (domain-general) parts.
Cross-area tactic transfer into cardinal and ordinal arithmetic. 6 Lean-verified new proofs from 4 schema transfers (40%). The deepest transfer is a proof-architecture transfer: a probability-theory pattern maps to a set-theory pattern with no shared identifiers — the connection is purely semantic.
Transfer to the sheaf-theoretic framework of Clausen and Scholze — designed to eliminate the measure-theoretic vocabulary probability depends on. 2 verified proofs from 10 attempts (20%). Central finding: a strictly better proof — a genuine improvement enabled by cross-area transfer.
Transfer into algebraic extensions, Galois groups, and finite fields. 4 verified proofs from 10 attempts (40%). All 10 schemas match the same target theorem — revealing a target attractor phenomenon where a single dominant proof state absorbs matches.
Transfer to circle homeomorphisms, ergodic theory, and measure-preserving transformations — the closest target to probability in the series. 4 Lean-verified proofs from 10 attempts (40%), split across substantive, genuine-but-narrow, and shallow transfer tiers.
Transfer to directed colimits, language embeddings, Skolem functions, and Presburger semilinear sets — with no measure-theoretic infrastructure. 5 proofs from 10 attempts (50%), the highest rate so far. Reveals a degenerate-attractor phenomenon motivating a minimum-entity-count filter for future target selection.
Transfer to entropy, divergence, and coding — both areas share probability’s measure-theoretic foundation. 9 Lean-verified proofs from 10 attempts (90%), the highest rate in the series by a wide margin. Confirms that shared infrastructure amplifies transfer success.
A negative-result paper on the paradigm boundary.
The first complete failure in the series: 0 transfers from 10 attempts (0%). All ten schemas fail for the same fundamental reason — they require type-class instances that categorical morphism and sheaf types do not carry. Identifies a hard paradigm boundary.
The paradigm boundary extends to homological algebra.
Second consecutive complete failure: 0 from 10 (0%). Confirms that the paradigm boundary identified in Part 8 extends beyond categorical sheaf theory into homological algebra. Contrast with Part 1 (same target, 40% from Probability) shows that source-area selection — not target-area difficulty — is the dominant factor.
Cumulative across the series: 90 schema attempts · 32 successes (36%) · 34 Lean-verified new proofs across at least 15 distinct theorems.