4 papers
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…