Gröbner Tactics
This repository contains Lean 4 tactics for the automated formal verification of Gröbner basis properties and computations.
Our main goal is to create powerful tactics that can automatically prove theorems related to Groebner Basis or the application of Groebner Basis within the Lean 4 theorem prover.
The foundational definitions and core theorems on which this work is built are developed in the companion project groebner_proj. One of the main technical challenges in Lean is that the standard MvPolynomial type is, in general, non-computable from the perspective of proof automation. To overcome this limitation, we introduce a dedicated implementation of computable polynomials that is suitable for execution and computation within Lean's kernel.
Both the library and its accompanying documentation are still under development.
Introduction
Workflow
- Lean to Externel Solvers: We extract mathematical objects (such as MvPolynomial and generators of Ideals) from the Lean context and employ meta-programming techniques, specifically Qq matching, or manual pattern matching, to deconstruct and analyze Lean expressions.
- External Computation: Gröbner basis–related computations on multivariate polynomials are delegated to externel solvers. The computed results are serialized into a structured JSON format and returned to Lean, where they are reinterpreted for subsequent verifications.
- Externel Solver to Lean: Lean parses the incoming JSON data into well-defined intermediate data structures. These structures are then systematically translated back into
Exprand ultimately elaborated intoTermobjects in Lean, allowing the externally computed results to be integrated into the proof environment. - Kernel Verification: The verification tasks are reduced to polynomial identity testing （PIT) problems which are discharged entirely within the Lean kernel using its internal computable polynomial representation.
Tactics
gb_solve:- Certifies that the remainder of a polynomial
upon reduction modulo a set is . - Verifies that a set
is a groebner basis of an ideal . - Decides whether a polynomial
belongs to an ideal . - Decides whether a polynomial
belongs to the radical ideal .
- Certifies that the remainder of a polynomial
idealeq: Verifies the equality of two ideals,add_gb_hyp: Automatically computes a Gröbner basisfor the ideal generated by using SageMath and adds the certified as a hypothesis in Lean.
Modes
Our tactic supports three modes: local SageMath computation (default), external SageMath computation (not recommended), and local SymPy computation.
-- local SageMath computation mode
example :
lex.IsRemainder (X 0 ^ 2 + X 1 ^ 3 + X 2 ^ 4 + X 3 ^ 5: MvPolynomial (Fin 4) ℚ)
{X 0, X 1, X 2, X 3} 0 := by
gb_solve
-- externel SageMath computation (API, not recommended)
set_option gb_tactic.backend 1 in
example :
lex.IsRemainder (X 0 ^ 2 + X 1 ^ 3 + X 2 ^ 4 + X 3 ^ 5: MvPolynomial (Fin 4) ℚ)
{X 0, X 1, X 2, X 3} 0 := by
gb_solve
-- local Sympy computation
set_option gb_tactic.backend 2 in
example :
lex.IsRemainder (X 0 ^ 2 + X 1 ^ 3 + X 2 ^ 4 + X 3 ^ 5: MvPolynomial (Fin 4) ℚ)
{X 0, X 1, X 2, X 3} 0 := by
gb_solve
Some Example
gb_solve
Given a polynomial gb_solve tactic automatically certifies the remainder of
-- Certifies that the remainder of a polynomial $f$ upon reduction modulo a set $B$ is $r$
example :
lex.IsRemainder (X 0 * X 1 : MvPolynomial (Fin 3) ℚ)
{2 * X 0 - X 1}
(C (1/2 : ℚ) * X 1 ^ 2) := by
gb_solve
The tactic can formally verify if a given set of polynomials constitutes a Gröbner basis for a specific ideal.
Here, it proves that
-- Verifies that a set $B$ is a groebner basis of an ideal $I$
example :
lex.IsGroebnerBasis
({1} : Set <| MvPolynomial (Fin 3) ℚ)
(Ideal.span ({X 0, 1 - X 0} : Set <| MvPolynomial (Fin 3) ℚ)) := by
gb_solve
The tactic can automatically decide and prove whether a given polynomial
-- Decides a polynomial $f$ belongs to an ideal $I$
example :
X 0 ∈ Ideal.span ({X 0, X 1} : Set (MvPolynomial (Fin 2) ℚ)) := by
gb_solve
In this example, it proves that
-- Decides a polynomial $f$ doesn't belong to an ideal $I$
example :
X 2 ∉ Ideal.span ({X 0 + X 1^ 2, X 1 ^ 2} : Set (MvPolynomial (Fin 3) ℚ)) := by
gb_solve
Beyond standard ideals, the tactic can determine if a polynomial
-- Decides a polynomial $f$ belongs to the radical ideal $\sqrt{I}$
example :
X 0 * X 1 ∈ (Ideal.span ({C (1/2 : ℚ) * (X 0 + X 1), C (1/2 : ℚ) * (X 0 - X 1)} :
Set (MvPolynomial (Fin 2) ℚ))).radical := by
gb_solve
Conversely, it correctly determines that
-- Decides a polynomial $f$ doesn't belong to the radical ideal $\sqrt{I}$
example :
X 0 ∉ (Ideal.span ({X 0 + X 1} : Set (MvPolynomial (Fin 3) ℚ))).radical := by
gb_solve
idealeq
The idealeq tactic automates the proof of equality between two polynomial ideals. It internally computes and compares their Gröbner bases to determine if the ideals generated by two different sets of polynomials are mathematically identical.
In the example below, it automatically verifies that the ideal generated by
example :
Ideal.span ({X 0 + X 1^2, X 1 }) =
Ideal.span ({X 0, X 1 } : Set (MvPolynomial (Fin 3) ℚ)) := by
idealeq
add_gb_hyp
Instead of directly closing a goal, the add_gb_hyp tactic computes the Gröbner basis for a specified set of polynomials and injects this fact as a new hypothesis into the local proof context. This is particularly useful when the Gröbner basis property is required as an intermediate step for further manual reasoning.
In this example, calling add_gb_hyp h calculates the Gröbner basis for the ideal generated by h stating that this basis is h exactly matches and closes the goal.
example : lex.IsGroebnerBasis ({X 0, X 1} :
Set (MvPolynomial (Fin 3) ℚ)) (Ideal.span {X 0, X 0 + X 1}) := by
add_gb_hyp h ({X 0, X 0 + X 1} : Set (MvPolynomial (Fin 3) ℚ))
simp only [ne_eq, one_ne_zero, not_false_eq_true, div_self, C_1, Fin.isValue, pow_one, one_mul,
zero_add] at h
exact h
Build
If you don't already have Lean 4 set up, please follow the official Lean 4 installation instructions.
Once Lean is installed, you can clone this repository and build the project:
git clone https://github.com/WuProver/GroebnerTactic.git
cd GroebnerTactic
lake exe cache get
lake build
If you want to use Sagemath as an external calculation tool, please follow the official SageMath installation instructions.
If you find that SageMath takes up too much storage space, or that installing SageMath on Windows is too cumbersome, you can opt to use SymPy as an external computation tool.
For Linux/MacOS systems, please run the following command:
python -m venv newenv
source newenv/bin/activate
pip install -r requirements.txt
For Windows CMD, please run the following command:
python -m venv newenv
newenv\Scripts\activate.bat
pip install -r requirements.txt
For Windows Powershell, please run the following command:
python -m venv newenv
.\newenv\Scripts\Activate.ps1
pip install -r requirements.txt
Installation
To use our tactics in your Lean 4 project, you need to add this repository as a dependency. Adding he following block to your project's lakefile.toml:
[[require]]
name = "GroebnerTactic"
git = "https://github.com/WuProver/GroebnerTactic.git"
scope = "WuProver"
rev = "main"
To use the full features, please download Sage as instructed above. Since installing Sage on Windows can be quite cumbersome, you can install Python instead and run the following commands.
python -m venv newenv
source newenv/bin/activate
pip install -r .lake/packages/GroebnerTactic/requirements.txt
If you prefer not to install anything, you can use the API mode, but please use it sparingly.