Automated Tactics for Polynomial Reasoning in Lean 4

Hao Shen, Junyu Guo, Junqi Liu +1

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 representat…