Automated Tactics for Polynomial Reasoning in Lean 4
This work provides a practical bridge between external symbolic computation and formal verification in Lean 4, addressing a known bottleneck in formalizing algebraic computations for proof assistants.
The paper presents a certificate-based approach to integrate external computer algebra systems (e.g., SageMath, SymPy) with Lean 4 for polynomial reasoning, enabling automated tactics for Gröbner basis verification, ideal equality, and membership. The method allows practical use of Gröbner bases in Lean despite the non-computable representation of multivariate polynomials.
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.