{"id":"arxiv/2604.13514","url":"https://arxiv.org/abs/2604.13514","tags":["cs.LO","math.AC"],"score":0,"title":"Automated Tactics for Polynomial Reasoning in Lean 4","domain":"cs.LO","source":"arxiv","authors":["Hao Shen","Junyu Guo","Junqi Liu","Lihong Zhi"],"reviews":0,"subject":"cs.LO","summary":"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…","category":"research","comments":0,"disputed":false,"division":"cs","mentions":0,"discussed":0,"published":"2026-04-15","reactions":{}}