The Jacobian conjecture is a famous open problem in mathematics asking whether a polynomial map between planes must be invertible (an automorphism) if its Jacobian determinant, a certain quantity measuring local stretching, is everywhere nonzero. In the classical setting over fields like the real or complex numbers, this remains unsolved after decades of effort. Over fields with positive characteristic, meaning fields where adding a prime number p to itself gives zero, mathematicians have studied modified versions of the conjecture. One such version, called the separable Jacobian conjecture, asks whether a polynomial map with Jacobian determinant equal to 1 must be an automorphism, provided the associated field extension is separable, a technical condition ruling out certain badly behaved extensions that only arise in positive characteristic.
The paper constructs an explicit polynomial map of the two-dimensional plane over the algebraic closure of the field with two elements, meaning characteristic two. The map is given by two specific polynomials P and Q in variables x and y. The authors show that the Jacobian determinant of this map equals 1 and that the field extension it induces is separable, so the map satisfies all the hypotheses of the separable Jacobian conjecture. However, three distinct points in the plane all get sent to the same image point, which means the map is definitely not invertible. This is a direct counterexample to the conjecture, and importantly it lives in dimension two, the simplest possible setting where such a map can be nontrivial.
The proof involves several interconnected arguments. The authors show that the degree of the field extension is exactly 3, meaning generically three points map to each location, even though the local Jacobian condition suggests invertibility. They trace the construction back to a three-variable map due to another mathematician, Irit Huq-Kuruvilla, and use a coordinate permutation to derive their example. The paper also includes careful analysis connecting algebraic function field theory to the geometric behavior of the map. An appendix discusses attempts to formally verify parts of the proof using computer-assisted proof assistants, noting both what was successfully formalized and where the boundaries of that verification lie.