Automated Tactics for Polynomial Reasoning in Lean 4
Hao Shen, Junyu Guo, Junqi Liu, Lihong Zhi
cs.LO
Apr 15, 2026 · v1
TL;DR
Certificate-based Lean 4 tactics that import and verify external Gröbner-basis computations.
Abstract
Applying Gröbner basis theory to concrete problems in Lean 4 remains difficult since the current formalization of multivariate polynomials is based on a non-computable representation and is therefore not suitable for efficient symbolic computation. As a result, computing Gröbner bases directly inside Lean is impractical for realistic examples. To address this issue, we propose a certificate-based approach that combines external computer algebra systems, such as SageMath or SymPy, with formal verification in Lean 4. Our approach uses a computable representation of multivariate polynomials in Lean to import and verify externally generated Gröbner basis computations. The external solver carries out the main algebraic computations, while the returned results are verified inside Lean. Based on this method, we develop automated tactics that transfer polynomial data between Lean and the external system and certify the returned results. These tactics support tasks such as remainder verification, Gröbner basis checking, ideal equality, and ideal or radical membership. This work provides a practical way to integrate external symbolic computation into Lean 4 while preserving the reliability of formal proof.
Problem
Applying Groebner basis theory in Lean 4 is impractical because the current formalization of multivariate polynomials uses a non-computable representation, making direct symbolic computation infeasible.
Approach
The authors propose a certificate-based approach that delegates heavy algebraic computation to external computer algebra systems (SageMath, SymPy) and verifies the returned results in Lean 4 using a computable polynomial representation. Automated tactics transfer polynomial data between Lean and the external solver, then certify the results. The approach supports remainder verification, Groebner basis checking, ideal equality, and ideal/radical membership.
Results
The tactics provide a practical integration of external symbolic computation into Lean 4 while preserving formal proof guarantees. Tasks such as Groebner basis verification and ideal membership can now be discharged automatically in Lean 4 for realistic examples that were previously intractable.
