{"id":"arxiv/2604.14912","url":"https://arxiv.org/abs/2604.14912","tags":["math.AC","cs.LO"],"score":0,"title":"Formalizing Wu-Ritt Method in Lean 4","domain":"math.AC","source":"arxiv","authors":["Yuxuan Xiao","Hao Shen","Junyu Guo","Dingkang Wang","Lihong Zhi"],"reviews":0,"subject":"math.AC","summary":"We formalize the Wu-Ritt characteristic set method for the triangular decomposition of polynomial systems in the Lean 4 theorem prover. Our development includes the core algebraic notions of the method, such as polynomial initials, orders, pseudo-division, pseudo-remainders with respect to a polynomial or a triangular set, and standard and weak ascending sets. On this basis, we formalize algorithms for computing basic sets, characteristic sets, and zero decompositions, and prove their termination and correctness. In particular, we formalize the well-ordering principle relating a polynomial…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-04-16","reactions":{}}