Cover Image

Automated Tactics for Polynomial Reasoning in Lean 4

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Shen, Hao, Guo, Junyu, Liu, Junqi, Zhi, Lihong
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science Commutative Algebra
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Formalizing Gröbner Basis Theory in Lean
by: Guo, Junyu, et al.
Published: (2026)

Formalizing Wu-Ritt Method in Lean 4
by: Xiao, Yuxuan, et al.
Published: (2026)

Formalization of Auslander--Buchsbaum--Serre criterion in Lean4
by: Guan, Naillin, et al.
Published: (2025)

Computability of Equivariant Gröbner bases
by: Ghosh, Arka, et al.
Published: (2025)

Polynomials as terms and the Boolean Independence Theorem
by: Klazar, M.
Published: (2024)

Formalizing Polynomial Laws and the Universal Divided Power Algebra
by: Chambert-Loir, Antoine, et al.
Published: (2025)

The transcendence degree of the reals over certain set-theoretical subfields
by: Fatalini, Azul, et al.
Published: (2024)

Derivations and gt-henselian field topologies
by: Walsberg, Erik
Published: (2025)

Specialization of Difference Equations and High Frobenius Powers
by: Dor, Yuval, et al.
Published: (2022)

Model theory of differential-henselian pre-$H$-fields
by: Pynn-Coates, Nigel
Published: (2019)

Bounded morphisms
by: Wagner, Frank Olaf
Published: (2015)

Tame pairs of transseries fields
by: Pynn-Coates, Nigel
Published: (2024)

The Regular Element Property in Constructive Mathematics
by: Coquand, Thierry
Published: (2024)

Dimension and topology in transserial tame pairs
by: Pynn-Coates, Nigel
Published: (2025)

Contracting Endomorphisms of Valued Fields
by: Dor, Yuval, et al.
Published: (2023)

Beyond the Fontaine-Wintenberger theorem
by: Jahnke, Franziska, et al.
Published: (2023)

When is the étale open topology a field topology?
by: Dittmann, Philip, et al.
Published: (2022)

Analytic Nullstellensätze and the model theory of valued fields
by: Aschenbrenner, Matthias, et al.
Published: (2022)

A Formalization of Divided Powers in Lean
by: Chambert-Loir, Antoine, et al.
Published: (2025)

Linear equations with monomial constraints and decision problems in abelian-by-cyclic groups
by: Dong, Ruiwen
Published: (2024)

A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4
by: Ramos, Arthur F., et al.
Published: (2026)

Quasipolynomial behavior via constructibility in multigraded algebra
by: Dao, Hailong, et al.
Published: (2025)

Geometric theories for real number algebra without sign test or dependent choice axiom
by: Lombardi, Henri, et al.
Published: (2024)

Approximation properties of torsion classes
by: Cox, Sean, et al.
Published: (2024)

Vopěnka's Principle, Maximum Deconstructibility, and singly-generated torsion classes
by: Cox, Sean
Published: (2024)

The étale open topology over the fraction field of a henselian local domain
by: Johnson, Will, et al.
Published: (2021)

Expressive Power of Infinitary Logic and Absolute co-Hopfianity
by: Asgharzadeh, Mohsen, et al.
Published: (2023)

Failure of singular compactness for Hom
by: Asgharzadeh, Mohsen, et al.
Published: (2025)

Automorphisms of valued Hahn groups
by: Kuhlmann, Salma, et al.
Published: (2023)

Azumaya algebras and Barr Theorem
by: Coquand, Thierry, et al.
Published: (2023)

L-Mosaics and Bounded Join-Semilattices in Isabelle/HOL
by: Linzi, Alessandro
Published: (2025)

The Ideal Membership Problem and Abelian Groups
by: Bulatov, Andrei A., et al.
Published: (2022)

Serre depth and local cohomology
by: Ficarra, Antonino
Published: (2026)

Normalizing Asymptotic Differential Equations
by: Aschenbrenner, Matthias, et al.
Published: (2024)

Material Interpretation and Constructive Analysis of Maximal Ideals in $\mathbb{Z}[X]$
by: Wiesnet, Franziskus
Published: (2025)

Closed bounded sets in 1-h-minimal valued fields
by: López, Juan Pablo Acosta
Published: (2024)

Formalizing Mason-Stothers Theorem and its Corollaries in Lean 4
by: Baek, Jineon, et al.
Published: (2024)

On cohomology of locally profinite sets
by: Aoki, Ko
Published: (2024)

An Algorithm for Diagonalizing Matrices of Formal Power Series
by: Dai, Zihao, et al.
Published: (2026)

Solving Polynomial Systems with Gröbner Bases: An Introduction to F4 and FGLM
by: Bigatti, Anna Maria, et al.
Published: (2025)