4 papers
math.FA2026
A Dimension-Independent Commutator Bound
Hao Shen, Jiaqi Wang, Lihong Zhi
We prove that every trace-zero matrix admits a representation with and ,…
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{…
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 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…