{"id":"palomar/PALOMAR-2026-08-27-000013","url":"https://github.com/Arthur742Ramos/jacobian-conjecture-lean/tree/8db55ea3ffa8ba90094d6ef78ee3351ddfce01ca","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-08-27-000013-v1.json","repo":"https://github.com/Arthur742Ramos/jacobian-conjecture-lean","tags":["math.AG","math.LO","msc:14R15","msc:03B35","algebraic-geometry","lean","jacobian-conjecture","polynomial-maps"],"score":0,"title":"Arthur742Ramos/jacobian-conjecture-lean","trust":"high","domain":"math.AG","source":"palomar","authors":["Arthur Freitas Ramos","David Barros Hulak","Ruy J. G. B. de Queiroz"],"reviews":0,"subject":"math.AG","summary":"An independent Lean 4 and Mathlib formalization of the explicit three-dimensional polynomial map announced by Levent Alpöge in 2026. The project proves that its formal Jacobian determinant is the nonzero constant -2, verifies an explicit three-point fibre over the complex numbers, and derives the failure of injectivity required to refute the dimension-three Jacobian conjecture. The source formulas and proof scope are recorded explicitly; no claim is made about the still-open two-dimensional case.","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-08-27","reactions":{},"formalized":true,"formalizes":[{"title":"An explicit counterexample to the Jacobian conjecture","identifier":"https://x.com/__alpoge__/status/2079028340955197566","relationship":"formalizes"}]}