arxiv: 2604.13514 · v1 · submitted 2026-04-15 · 💻 cs.LO · math.AC

Recognition: unknown

Automated Tactics for Polynomial Reasoning in Lean 4

Hao Shen , Junyu Guo , Junqi Liu , Lihong Zhi

Authors on Pith no claims yet

Pith reviewed 2026-05-10 12:39 UTC · model grok-4.3

classification 💻 cs.LO math.AC

keywords Lean 4Gröbner basismultivariate polynomialscertificate verificationautomated tacticsformal verificationsymbolic computationideal membership

0 comments

The pith

A computable representation of multivariate polynomials lets Lean 4 verify Gröbner basis certificates produced by external solvers.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper addresses the impracticality of computing Gröbner bases inside Lean 4 due to its non-computable polynomial representation. It introduces a certificate-based method that shifts the main algebraic work to external systems such as SageMath or SymPy while using a new computable encoding to check the results inside Lean. Automated tactics then handle data transfer and certification for remainder verification, Gröbner basis checking, ideal equality, and ideal or radical membership. A sympathetic reader cares because the approach preserves formal reliability while accessing efficient symbolic computation for realistic examples.

Core claim

The paper establishes that a computable representation of multivariate polynomials in Lean 4 can import and formally verify Gröbner basis computations performed by external computer algebra systems. The external solver handles the primary algebraic calculations, and the returned certificates are checked inside Lean to support tasks such as remainder verification, Gröbner basis checking, ideal equality, and ideal or radical membership.

What carries the argument

The computable representation of multivariate polynomials that enables importing and verifying externally generated Gröbner basis computations.

If this is right

Automated tactics become available inside Lean 4 for remainder verification without performing the full computation internally.
Gröbner basis checking and certification can be performed reliably on realistic examples.
Ideal equality and ideal or radical membership tests can be automated via verified external certificates.
Polynomial reasoning in formal proofs can scale beyond what direct internal computation allows while maintaining soundness.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

The same certificate pattern could be adapted to other interactive theorem provers that face computability limits on algebraic structures.
Extending the set of supported external systems would increase the range of solvable polynomial problems.
Optimizing the verification step inside Lean might reduce overhead for very large inputs.

Load-bearing premise

The computable representation of multivariate polynomials is sufficient to detect any errors or omissions in certificates from the external systems for the supported tasks.

What would settle it

A concrete multivariate polynomial ideal for which an external Gröbner basis certificate is accepted by the Lean tactic but is algebraically incorrect, or a correct certificate that the tactic rejects.

read the original 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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper gives Lean 4 users workable tactics to verify Gröbner basis results from Sage or SymPy using a computable polynomial representation.

read the letter

The main point is that they created automated tactics in Lean 4 that move the actual Gröbner basis work to an external CAS and then check the output inside the prover. This gets around the fact that Lean's standard multivariate polynomial type is non-computable and therefore too slow for direct symbolic computation on anything realistic. The tactics cover remainder verification, basis checking, ideal equality, and ideal or radical membership by importing data and certifying it against the computable representation they set up in Lean. That part is new for Lean 4 and fills a practical gap that earlier formalizations left open. The method itself is standard certificate checking, but the paper shows how to wire it up for these specific tasks without circularity, since the verification step is independent of the external solver. The approach is clean and the high-level soundness argument holds up. The soft spots are mostly about depth rather than fatal problems. The abstract stays at the level of describing the method and the supported tasks, so concrete examples, performance numbers on non-trivial inputs, or discussion of interface edge cases would help. If the full paper has only small demonstrations, the claim of practicality stays a bit thin. The citation pattern looks reasonable and draws on prior certificate work in other systems. This is for people who already use Lean for algebra and need to handle polynomials without hitting the representation wall. A reader working on formal computer algebra or proof assistant integrations will get direct value from the implementation choices. It is worth sending to peer review because it addresses a real usability issue with a reproducible, checkable solution rather than hand-waving.

Referee Report

0 major / 3 minor

Summary. The manuscript proposes a certificate-based integration of external computer algebra systems (SageMath, SymPy) with Lean 4 for polynomial reasoning. It introduces a computable representation of multivariate polynomials to import and formally verify Gröbner basis computations performed externally, enabling automated tactics for remainder verification, Gröbner basis checking, ideal equality, and ideal or radical membership. The external solver handles heavy computation while Lean verifies the results to preserve formal guarantees.

Significance. If the implementation details and verification procedures hold, this provides a practical bridge between efficient symbolic computation and formal verification in Lean 4, addressing the limitation of its current non-computable polynomial formalization. The certificate-based approach is a standard, sound strategy that offloads computation while retaining proof-assistant reliability; explicit credit is due for focusing on verifiable certificates rather than reimplementing CAS algorithms inside Lean.

minor comments (3)

The abstract and introduction would benefit from a short concrete example (e.g., a single polynomial ideal membership query with the corresponding tactic invocation and output) to illustrate the workflow before the high-level description.
Section describing the computable polynomial representation should include a brief comparison table or complexity discussion against the existing non-computable Lean mathlib version to clarify performance gains.
The paper should cite recent related work on certificate-based Gröbner basis verification in other proof assistants (e.g., Coq or Isabelle) for context.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive assessment of the manuscript, the accurate summary of our certificate-based approach, and the recommendation for minor revision. We appreciate the recognition that this work provides a practical integration of external symbolic computation with formal verification in Lean 4 while preserving soundness.

Circularity Check

0 steps flagged

No significant circularity; approach relies on independent external verification checked inside Lean

full rationale

The paper identifies the non-computable nature of Lean's existing multivariate polynomial formalization as a limitation and proposes a certificate-based workflow that offloads Gröbner basis computation to external CAS (SageMath/SymPy) while verifying the returned certificates against a computable representation inside Lean 4. This verification step for remainder, basis checking, ideal equality, and membership is independent of the external solver's internal algorithms and does not reduce to a self-definition, fitted parameter renamed as prediction, or load-bearing self-citation. No equations or uniqueness theorems are invoked that collapse back to the paper's own inputs. The derivation chain is therefore self-contained against external benchmarks.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on the existence of a suitable computable polynomial representation in Lean and on the ability of that representation to verify certificates from external systems for the listed algebraic tasks.

axioms (1)

domain assumption External computer algebra systems produce certificates that can be verified for correctness inside Lean using the computable polynomial representation.
The entire method depends on this transfer and verification step being sound for Gröbner basis computations and the supported tasks.

pith-pipeline@v0.9.0 · 5486 in / 1339 out tokens · 27272 ms · 2026-05-10T12:39:24.017895+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

16 extracted references · 4 canonical work pages · 1 internal anchor

[1]

Buchberger, B.: Bruno Buchberger’s PhD thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimen- sional polynomial ideal. Journal of Symbolic Computation41(3), 475–511 (2006).https://doi.org/https://doi.org/10.1016/j.jsc.2005.09.007, https://www.sciencedirect.com/science/article/pii/S0747717105001483, logic, Mathe...

work page doi:10.1016/j.jsc.2005.09.007 1965
[2]

Springer Science & Business Media (2013)

Char, B.W., Geddes, K.O., Gonnet, G.H., Leong, B.L., Monagan, M.B., Watt, S.: Maple V library reference manual. Springer Science & Business Media (2013)

2013
[3]

Springer (1997)

Cox, D., Little, J., O’shea, D., Sweedler, M.: Ideals, varieties, and algorithms. Springer (1997)

1997
[4]

Journal of Symbolic Computation39(5), 569–592 (2005)

Delahaye, D., Mayero, M.: Dealing with algebraic expressions over a field in Coq using Maple. Journal of Symbolic Computation39(5), 569–592 (2005)

2005
[5]

Ebner, G.: quote4: Intuitive, type-safe expression quotations for Lean 4 (2022), https://github.com/leanprover-community/quote4

2022
[6]

Guo, J., Shen, H., Liu, J., Zhi, L.: Formalizing Gröbner basis theory in Lean (2026), https://arxiv.org/abs/2602.12772

work page internal anchor Pith review Pith/arXiv arXiv 2026
[7]

Guo,J., Shen, H.,Zhi,L., Liu, J.:MonomialOrderedPolynomial: Monomialordered polynomial implementation in Lean 4 (2026),https://github.com/WuProver/ MonomialOrderedPolynomial

2026
[8]

In: International Conference on Theorem Proving in Higher Order Logics

Harrison, J.: HOL light: An overview. In: International Conference on Theorem Proving in Higher Order Logics. pp. 60–66. Springer (2009)

2009
[9]

Journal of Automated Reasoning66(2), 215–238 (2022)

Lewis, R.Y., Wu, M.: A bi-directional extensible interface between Lean and Math- ematica. Journal of Automated Reasoning66(2), 215–238 (2022)

2022
[10]

PeerJ Computer Science3, e103 (2017)

Meurer, A., Smith, C.P., Paprocki, M., Čertík, O., Kirpichev, S.B., Rocklin, M., Kumar, A., Ivanov, S., Moore, J.K., Singh, S., et al.: SymPy: symbolic computing in Python. PeerJ Computer Science3, e103 (2017)

2017
[11]

de Moura, S

Moura, L., Ullrich, S.: The Lean 4 theorem prover and programming lan- guage. In: Automated Deduction – CADE 28: 28th International Conference on Automated Deduction, Virtual Event, July 12–15, 2021, Proceedings. p. 625–635. Springer-Verlag, Berlin, Heidelberg (2021).https://doi.org/10.1007/ 978-3-030-79876-5_37,https://doi.org/10.1007/978-3-030-79876-5_37

work page doi:10.1007/978-3-030-79876-5_37 2021
[12]

Sage Developers: SageMath, the sage mathematics software system (2020)

2020
[13]

In: International Conference on Intelligent Com- puter Mathematics

Seddiki, O., Dunchev, C., Khan-Afshar, S., Tahar, S.: Enabling symbolic and nu- merical computations in hol light. In: International Conference on Intelligent Com- puter Mathematics. pp. 353–358. Springer (2015)

2015
[14]

The Coq Development Team: Coq (2002),https://coq.inria.fr

2002
[15]

https: //doi.org/10.1145/3372885.3373824 .https://doi.org/10.1145/3372885.3373824 15

The mathlib community: The Lean mathematical library. In: CPP 2020. p. 367–381. Association for Computing Machinery, New York, NY, USA (2020). https://doi.org/10.1145/3372885.3373824,https://doi.org/10.1145/ 3372885.3373824

work page doi:10.1145/3372885.3373824 2020
[16]

Wolfram Research, Inc

Wolfram, S.: The mathematica book. Wolfram Research, Inc. (2003)

2003