Gröbner Tactics
Certificate-based tactics that connect external symbolic computation with kernel-checked polynomial reasoning in Lean 4.
Certificate-Based Polynomial Reasoning
Computing Gröbner bases directly within Lean 4 is impractical for realistic examples because its standard multivariate-polynomial representation is not designed for efficient symbolic computation. Gröbner Tactics delegates the main algebraic computation to SageMath or SymPy, then imports the result into Lean's computable polynomial representation and verifies the returned certificate inside the kernel.
Verification Workflow
The external solver accelerates computation, but Lean remains the final authority: only results that can be checked against the imported certificate become part of the formal proof.
-
01
Extract
Read multivariate polynomials and ideal generators from the Lean proof context.
-
02
Compute
Delegate Gröbner-basis computation to SageMath or SymPy.
-
03
Import
Return the computed result to Lean as structured certificate data.
-
04
Verify
Discharge the resulting polynomial identities within the Lean kernel.
Supported Goals
The tactic suite turns common Gröbner-basis proof obligations into formally verified Lean results.
gb_solveCertifies polynomial reductions, Gröbner-basis properties, ideal membership, and radical-ideal membership.idealeqVerifies equality between polynomial ideals.add_gb_hypComputes a Gröbner basis and introduces its certified property into the local Lean context.