SparseProduct Lean Formalization

This repository contains the Lean 4 formalization for the sparse polynomial product results in paper Quasi-linear Time Multiplication of Sparse Polynomials with Integer Coefficients. The repository has two complementary parts: a Maple worksheet validating the counterexample in Section 2, "The failed probability claim", and Lean files formalizing the core positive results from Sections 3 and 4.

The current development is checked with Lean 4.29.0 and mathlib v4.29.0. The project no longer depends on cslib; all retained Lean code is under SparseProduct/ and is imported through the root file SparseProduct.lean.

Build

lake exe cache get
lake build

The current build succeeds on Lean 4.29.0. A successful run may still report Lean warnings for unused local variables, but there are no anonymous sorry proof holes in the retained SparseProduct code.

Layout

• SparseProduct.lean: root import for the formalization.
• SparseProduct/Foundations.lean: shared definitions for sparsity, integer coefficient height, the supplied height bound, and soft-O predicates.
• SparseProduct/SuppliedOutputSparsity.lean: the formal counterpart of the supplied-output-sparsity theorem. Its main theorem is SuppliedOutputSparsity.suppliedOutputSparsityTheorem.
• SparseProduct/SparseProductCyclicImage.lean: cyclic-image identities, prime-isolation and candidate-filtering scaffolding, and the top-level theorems SparseProduct.SparseProductCyclicImage.finiteFieldSparseProduct and SparseProduct.SparseProductCyclicImage.integerSparseProductReduction.
• SparseProduct/RandomizedAlgorithms.lean: named black-box Monte Carlo statements used by the top-level sparse-product theorems.
• Counterexample.mw: Maple worksheet accompanying Section 2 of the paper. It records the computational counterexample to a probability claim in prior work, including the enumeration of polynomial pairs and the distribution of distinct T_p values over the sampled primes. This file is supporting computational evidence and is not imported by SparseProduct.lean.

Paper Correspondence

• Section 2, "The failed probability claim": Counterexample.mw validates the counterexample to Lemma 4.7(ii) of the prior Giorgi--Grenet--Perret du Cray analysis. This is a Maple verification artifact, not a Lean module.
• Section 3, "Multiplication with integer coefficients": the Lean theorem SuppliedOutputSparsity.suppliedOutputSparsityTheorem formalizes the supplied-output-sparsity integer result, namely the displayed ~O(T log(DH)) bit-complexity theorem for the univariate supplied-sparsity core.
• Section 4, "Multiplication with finite field coefficients": the Lean theorem SparseProduct.SparseProductCyclicImage.finiteFieldSparseProduct formalizes the large-characteristic finite-field sparse-product theorem. The same file also records SparseProduct.SparseProductCyclicImage.integerSparseProductReduction, the univariate integer reduction statement following the finite-field route.

The multivariate Kronecker-substitution wrapper and the product-verification wrapper for unknown output sparsity are not part of the current Lean formalization. They remain paper-level arguments around the univariate supplied-output and finite-field core theorems exposed through SparseProduct.lean.

Counterexample Worksheet

The paper's Section 2, "The failed probability claim", explains why a previously stated probability claim is false. The repository includes Counterexample.mw as the reproducible Maple worksheet for that discussion. It constructs the counterexample data, counts the number of distinct cyclic image products T_p obtained from pairs of polynomials, and tabulates the observed frequencies for the relevant primes. Since this worksheet is not Lean code, lake build does not check it; the formal Lean development remains under SparseProduct/.

Axiom Boundary

The retained development uses named axioms for imported external theorems and for randomized algorithmic results whose full formalization is outside the current project scope:

• ggprTheorem34
• ggprFact32
• monteCarlo_sparseProduct_finiteField_fieldOps
• monteCarlo_sparseProduct_finiteField
• monteCarlo_primeInInterval
• monteCarlo_sparseProduct_integer
• exists_sampling_primeSet
• uniformOfFinset_isolation_failure_bound
• uniformOfFinset_singleton_recover_bound

All other retained Lean declarations are definitions, lemmas, or theorems proved inside the project.