Characteristic Set

The goal of this project is to formalize the Characteristic Set Method (also known as Wu's Method) in the Lean 4 theorem prover. This project establishes the mathematical infrastructure for algebraic geometry based on triangular decomposition, bridging the gap between Lean and algorithmic methods for solving systems of multivariate polynomial equations.

This project is a work in progress; feedback, fixes, and suggestions are highly welcome.

Introduction

Definitions

• MvPolynomial.mainDegree: The multiset of occurrences of the largest variable in a polynomial. Its cardinality is the degree in that variable; it is empty for constants and zero.
• MvPolynomial.rank and TriangularSet.rank: The ranks used to order polynomials and triangular sets.
• MvPolynomial.pseudo and MvPolynomial.setPseudo: Pseudo-division by a polynomial or a triangular set.
• TriangularSet: A finite ordered sequence of nonzero polynomials with strictly increasing classes.
• TriangularSet.IsAscendingSet and TriangularSet.IsWeakAscendingSet: Ritt's strong ascending sets and Wu's weak ascending sets, respectively.
• AscendingSetTheory: An interface parameterized by the ascending-set predicate, providing the basic-set algorithm and its properties.
• MvPolynomial.List.basicSet: The minimal ascending set contained in a list of polynomials.
• MvPolynomial.List.characteristicSet: The characteristic set of a list of polynomials.
• MvPolynomial.List.zeroDecomposition: A list of triangular sets that decompose the zero set of a polynomial system.

Main Statements

Given a field $K$, an ordered finite index set $\sigma$, and a list of polynomials $PS \subseteq K[x_\sigma]$, we establish the following core results:

• MvPolynomial.List.basicSet_minimal: The computed basic set is minimal among ascending sets contained in the input list, for either ascending-set predicate.
• MvPolynomial.List.characteristicSet_isCharacteristicSet: The computed characteristic set $CS$ has zero pseudo-remainders for the input polynomials and satisfies $Zero(PS) \subseteq Zero(CS)$.
• MvPolynomial.List.vanishingSet_eq_zeroDecomposition_union: The zero set of a polynomial system is a finite union of quasi-varieties: $Zero(PS) = \bigcup_{CS \in \mathcal{ZD}} Zero(CS / \text{InitialProd}(CS))$.

Project Resources

We maintain a set of web-based resources to track and explore the formalization effort:

• 📘 Project Homepage

• 📐 Formalization Blueprint A detailed list of definitions, lemmas, and theorems, including their proof status and logical dependencies.

• 🔗 Dependency Graph A visual representation of the dependency structure of the formalized components.

These tools help us manage development, track progress toward formalization, and guide future contributors.

Build

To use this project, you'll need to have Lean 4 and its package manager lake installed. If you don’t already have Lean 4 set up, follow the Lean 4 installation instructions.

Once Lean is installed, you can clone this repository and build the project:

git clone https://github.com/WuProver/lean_characteristic_set.git
cd lean_characteristic_set
lake exe cache get
lake build

References

Wen-Tsun, W. Mathematics Mechanization: Mechanical Geometry Theorem-Proving, Mechanical Geometry Problem-Solving and Polynomial Equations-Solving. Springer, 2001. https://link.springer.com/book/9780792358350

Wen-Tsun, W. Basic principles of mechanical theorem proving in elementary geometries. Journal of Automated Reasoning 2, 221–252 (1986). https://doi.org/10.1007/BF02328447