Automated Tactics for Polynomial Reasoning in Lean 4

TL;DR

This paper introduces a certificate-based method combining external computer algebra systems with Lean 4 to perform and verify polynomial computations like Gr"obner basis calculations efficiently and reliably.

Contribution

It presents automated tactics that facilitate importing, verifying, and certifying polynomial computations in Lean 4 using external algebra systems.

Findings

Developed tactics for transferring polynomial data between Lean and external systems.

Enabled verification of Gr"obner basis computations within Lean 4.

Supported tasks include ideal membership, equality, and radical membership verification.

Abstract

Applying Gr\"obner 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\"obner 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\"obner 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\"obner 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.