{"id":"palomar/PALOMAR-2026-11-03-000028","url":"https://github.com/zblore/fc-jacobian-poisson/tree/e395ab52d16b1c26b354daecf0c62b361f01c7a8","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-11-03-000028-v1.json","repo":"https://github.com/zblore/fc-jacobian-poisson","tags":["math.RA","math.AG","msc:14R15","msc:17B63"],"score":0,"title":"The Jacobian conjecture in dimension 2n implies the Poisson conjecture in dimension n","trust":"high","domain":"math.RA","source":"palomar","authors":["Zayn Blore"],"reviews":0,"subject":"math.RA","summary":"A machine-checked proof that, over a field of characteristic zero, the Jacobian conjecture in dimension 2n implies the Poisson conjecture in dimension n (K. Adjamagbo and A. van den Essen, 2007, Theorem 7). The statement and definitions are Formal Conjectures' (poisson_conjecture.variants.jacobian_implication in PoissonConjecture.lean, arXiv math/0608009), copied verbatim into Challenge.lean, so this entry proves Formal Conjectures' own statement. A Poisson endomorphism's Jacobian matrix lies in Mathlib's symplectic group, so its determinant is a unit; the Jacobian conjecture then gives a…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-11-03","reactions":{},"formalized":true,"formalizes":[{"title":"A proof of the equivalence of the Dixmier, Jacobian and Poisson conjectures","identifier":"https://arxiv.org/abs/math/0608009","relationship":"formalizes"}]}