Formal Resolution of the Two-Dimensional Jacobian Conjecture in Lean 4 via Graded Differential Operators.
-
Updated
Jul 28, 2026 - Lean
Formal Resolution of the Two-Dimensional Jacobian Conjecture in Lean 4 via Graded Differential Operators.
Polynomial Keller maps and certified transformations of them, including the Bass–Connell–Wright degree reduction.
An independent structural proof excluding the (72,108) case of the plane Jacobian Conjecture (GGHV, arXiv:2204.14178) — conditionally raising the counterexample degree bound from 108 to 125. Priority for the exclusion is B. Helali's (doi:10.5281/zenodo.21479814). Exact sympy checkers, spec-only auditors, Lean-certified core identity.
Add a description, image, and links to the polynomial-automorphisms topic page so that developers can more easily learn about it.
To associate your repository with the polynomial-automorphisms topic, visit your repo's landing page and select "manage topics."