7 papers
An Explicit Polynomial Counterexample to Connes' Embedding Conjecture
Jiaqi Wang, Lihong Zhi
We construct an explicit Hermitian polynomial in six selfadjoint variables, , with integer coefficients, degree , and exactly mon…
A Dimension-Independent Commutator Bound
Hao Shen, Jiaqi Wang, Lihong Zhi
We prove that every trace-zero matrix admits a representation with and ,…
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…
Whitney Stratification of Algebraic Boundaries of Convex Semi-algebraic Sets
Zihao Dai, Zijia Li, Zhi-Hong Yang +1
Algebraic boundaries of convex semi-algebraic sets are closely related to polynomial optimization problems. Building upon Rainer Sinn's work, we refine the stratification of iterat…
Synthesizing Invariants for Polynomial Programs by Semidefinite Programming
Hao Wu, Qiuye Wang, Bai Xue +3
Constraint-solving-based program invariant synthesis takes a parametric invariant template and encodes the (inductive) invariant conditions into constraints. The problem of charact…