Open Research Index

Arthur742Ramos/jacobian-conjecture-lean

Arthur Freitas Ramos, David Barros Hulak, Ruy J. G. B. de Queiroz

Palomar Registrypalomar/PALOMAR-2026-08-27-000013Aug 27, 2026math.AGscore 0

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.

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-08-27-000013
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-27-000013/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-08-27-000013/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'