Showing math.ACShow all
3 papers · 1 filter
math.AC2026
A Solution to Iima--Yoshino Problem 2.3
Junyu Guo, Hao Shen, Junqi Liu +1
Iima and Yoshino asked for an ideal in , with , and a monomial order such that $S/I\cong k[x_i:i\equiv\pm1\pmod5], \operatorname{…
math.AC2026
Formalizing Wu-Ritt Method in Lean 4
Yuxuan Xiao, Hao Shen, Junyu Guo +2
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…
math.AC2026
Formalizing Gröbner Basis Theory in Lean
Junyu Guo, Hao Shen, Junqi Liu +1
We present a formalization of Gröbner basis theory in Lean 4, built on top of Mathlib's infrastructure for multivariate polynomials and monomial orders. Our development covers the…