2 papers
cs.AI2026
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,…
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…