Lean 4 / Mathlib formalization of the algebraic core of WP28
src/WP28Algebra.lean (mirrored in the Lake project wp28proofs/Wp28proofs/WP28Algebra.lean) contains 27 machine-checked
statements, with no sorry, covering the deterministic parts of the proofs:
| Paper item | Lean theorems |
|---|---|
| Vandermonde constraints (eq. 4) for (1,2), (1,2,4), (1,2,4,8), (1,2,3); β_r and A_r (Table 2) | vandermonde_12/124/1248/123, beta_2/3/4, beta_3_pattern123, amp_2/3 |
| Theorem 2(ii): exact biases of J₂, J₃ | exact_bias_J2, exact_bias_J3 |
| Theorem 2(iv): Newton map, error identity, q-fold identity | newton_map, newton_error, newtonErr_closed |
| Theorem 2(iv): basin of attraction (convergence iff |u| < 1) | basinIter_abs, basin_converges, basin_diverges |
| Theorem 2(v): boundary constant algebra −θ₀(βc^r)^{2^q} | boundary_constant |
| Theorem 1 proof: exponent algebra of the frontier (√N m^{−r2^q} = 1 at α(r,q); negative power below) | frontier_exponent, frontier_below |
| Theorem 2(i): Gamma inverse moments from Γ(s+1) = sΓ(s); E R_n, E R_n², Var θ̂_n | gamma_inv_moment1/2, exponential_remainder_moments |
| Theorem 2(iii): Beta inverse moments as Gamma ratios; exact Var J₂ and E J₂ | beta_inverse_moments, var_J2_exact, mean_J2_exact |
Not formalized (and not claimed to be): the probabilistic statements (O_p bounds, Lemmas 3–7, the CLT/Slutsky steps of Theorems 1–3),
which depend on measure-theoretic infrastructure beyond the scope of this check; they are verified by SymPy (theory/symbolic_checks.py)
and by the Monte Carlo evidence.
Reproduce
bash
curl -sSf https://raw.githubusercontent.com/leanprover/elan/master/elan-init.sh | sh -s -- -y # once
cd theory/lean/wp28proofs && lake exe cache get && lake build # Lean 4 v4.35.0, Mathlib master (lake-manifest.json)lake build must end with Build completed successfully and no sorry warnings (bash scripts/check_lean.sh).