6 papers
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{…
MechGeo: Autoformalizing and Proving Euclidean Geometry in Lean 4
Hao Shen, Junyu Guo, Tian Cui +2
We present MechGeo, a Mathlib native agentic framework that jointly addresses faithful autoformalization and certified proof construction for Euclidean geometry. In this framework,…
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…
Automated Tactics for Polynomial Reasoning in Lean 4
Hao Shen, Junyu Guo, Junqi Liu +1
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 representati…
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…
Vector spaces over finite commutative rings
Jun Guo, Junli Liu, Qiuli Xu
Vector spaces over finite fields and Anzahl formulas of subspaces were studied by Wan (Geometry of Classical Groups over Finite Fields, Science Press, 2002). As a generalization, w…