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.
The Koras-Russell cylinder as an affine modification of A^4 — a commuting square through a motivic 4-sphere, a one-point Borel-Moore defect, and a machine-certified verification layer anyone can re-run in one command
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 affine-algebraic-geometry topic page so that developers can more easily learn about it.
To associate your repository with the affine-algebraic-geometry topic, visit your repo's landing page and select "manage topics."