Image de couverture de livre

Formalizing Wu-Ritt Method in Lean 4

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Xiao, Yuxuan, Shen, Hao, Guo, Junyu, Wang, Dingkang, Zhi, Lihong
Format:	Preprint
Publié:	2026
Sujets:	Commutative Algebra Logic in Computer Science
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

Formalizing Gröbner Basis Theory in Lean
par: Guo, Junyu, et autres
Publié: (2026)

Automated Tactics for Polynomial Reasoning in Lean 4
par: Shen, Hao, et autres
Publié: (2026)

Formalization of Auslander--Buchsbaum--Serre criterion in Lean4
par: Guan, Naillin, et autres
Publié: (2025)

Computability of Equivariant Gröbner bases
par: Ghosh, Arka, et autres
Publié: (2025)

A Formalization of Divided Powers in Lean
par: Chambert-Loir, Antoine, et autres
Publié: (2025)

A Prime-Generated Formalization of Nagata's Factoriality Theorem in Lean 4
par: Ramos, Arthur F., et autres
Publié: (2026)

Formalizing Polynomial Laws and the Universal Divided Power Algebra
par: Chambert-Loir, Antoine, et autres
Publié: (2025)

The transcendence degree of the reals over certain set-theoretical subfields
par: Fatalini, Azul, et autres
Publié: (2024)

Derivations and gt-henselian field topologies
par: Walsberg, Erik
Publié: (2025)

Specialization of Difference Equations and High Frobenius Powers
par: Dor, Yuval, et autres
Publié: (2022)

Model theory of differential-henselian pre-$H$-fields
par: Pynn-Coates, Nigel
Publié: (2019)

Bounded morphisms
par: Wagner, Frank Olaf
Publié: (2015)

Tame pairs of transseries fields
par: Pynn-Coates, Nigel
Publié: (2024)

The Regular Element Property in Constructive Mathematics
par: Coquand, Thierry
Publié: (2024)

Dimension and topology in transserial tame pairs
par: Pynn-Coates, Nigel
Publié: (2025)

Contracting Endomorphisms of Valued Fields
par: Dor, Yuval, et autres
Publié: (2023)

Beyond the Fontaine-Wintenberger theorem
par: Jahnke, Franziska, et autres
Publié: (2023)

When is the étale open topology a field topology?
par: Dittmann, Philip, et autres
Publié: (2022)

Analytic Nullstellensätze and the model theory of valued fields
par: Aschenbrenner, Matthias, et autres
Publié: (2022)

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

Polynomials as terms and the Boolean Independence Theorem
par: Klazar, M.
Publié: (2024)

Quasipolynomial behavior via constructibility in multigraded algebra
par: Dao, Hailong, et autres
Publié: (2025)

Formalizing Mason-Stothers Theorem and its Corollaries in Lean 4
par: Baek, Jineon, et autres
Publié: (2024)

An Algorithm for Diagonalizing Matrices of Formal Power Series
par: Dai, Zihao, et autres
Publié: (2026)

Geometric theories for real number algebra without sign test or dependent choice axiom
par: Lombardi, Henri, et autres
Publié: (2024)

Approximation properties of torsion classes
par: Cox, Sean, et autres
Publié: (2024)

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

The étale open topology over the fraction field of a henselian local domain
par: Johnson, Will, et autres
Publié: (2021)

Expressive Power of Infinitary Logic and Absolute co-Hopfianity
par: Asgharzadeh, Mohsen, et autres
Publié: (2023)

Failure of singular compactness for Hom
par: Asgharzadeh, Mohsen, et autres
Publié: (2025)

Automorphisms of valued Hahn groups
par: Kuhlmann, Salma, et autres
Publié: (2023)

Azumaya algebras and Barr Theorem
par: Coquand, Thierry, et autres
Publié: (2023)

On the equivalence problem of Smith forms for multivariate polynomial matrices
par: Lu, Dong, et autres
Publié: (2024)

L-Mosaics and Bounded Join-Semilattices in Isabelle/HOL
par: Linzi, Alessandro
Publié: (2025)

The Ideal Membership Problem and Abelian Groups
par: Bulatov, Andrei A., et autres
Publié: (2022)

Serre depth and local cohomology
par: Ficarra, Antonino
Publié: (2026)

Normalizing Asymptotic Differential Equations
par: Aschenbrenner, Matthias, et autres
Publié: (2024)

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

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

On cohomology of locally profinite sets
par: Aoki, Ko
Publié: (2024)