Proved
Formal polynomial counterexample reported complete ↗
The pinned algebraic statements, not an analytic derivative identification.
Observed Oct 13, 2026
Theorem · version 2
No polynomial inverse for the three-variable witness
Statement
There exists a polynomial map F: → with constant Jacobian determinant −2 and no two-sided polynomial compositional inverse.
Assumptions
- Polynomial maps and composition are taken over ℚ.
Scope
The source witnesses this existence statement using the three-variable counterexample. Analytic derivative correspondence and further geometric interpretations are outside this formal result.
Evidence
Source reports
Formal proofs
Lean: no polynomial inverse for the rational witness ↗
Complete formal proof reported externally
The endpoint witnesses the statement over ℚ with three variables. The explicit rational points also give the complex non-injectivity; analytic correspondence was not formalized by this project.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Declaration & revision
Alpoge.FormalConjecturesJC.jacobian_conjecture_falseCommit b8eec94711a9b73151929b78cbd7cb999a008590
Connections
In this problem · publication v5 · Selected context
Jacobian conjecture →
Supporting result · Proved
Relationship not independently reviewed. This concerns its use in this problem.
In this problem · publication v8
Jacobian conjecture →
Supporting result · Proved
Relationship not independently reviewed. This concerns its use in this problem.
Sources
Alpöge counterexample in Lean →
- README trust boundary; Alpoge/Basic.lean and Alpoge/FormalConjectures.lean → · Original passage ↗
Recorded wording
The source proves constant formal polynomial Jacobian determinant, a three-point fiber, and failure of a polynomial inverse for the recorded Jacobian conjecture statement.
paraphrase · OpenMath supplies original paraphrases and links; no proof text is republished.
alerad/alpoge-lean project · Project documentation · Publication date Jul 23, 2026
Public formal source; build and independent mathematical review are separate checks.
Alpöge counterexample in Lean — pinned source ↗No OpenMath execution recorded
Public source inspected for statement and assumptions; this proof project has not been executed by OpenMath.
Revision & attribution
Source revision: b8eec94711a9b73151929b78cbd7cb999a008590. Observed Oct 13, 2026.
The project reports an AI-assisted formalization and computer-algebra workflow; this is distinct from the original discovery.
Source updated Jul 23, 2026.
Alpöge counterexample in Lean — pinned source: b8eec94711a9b73151929b78cbd7cb999a008590.
History
Statement versions
Statement versions and problem publication versions are separate. A new publication can update context or sources while retaining the same statement.
Assessment history · 1
Assessments retained in these publication records. Earlier statement versions retain their own source histories.
Proved
Formal polynomial counterexample reported complete ↗
The pinned algebraic statements, not an analytic derivative identification.
Observed Oct 13, 2026 · Source passage →
Record details
- Claim ID
- claim-jacobian-no-polynomial-inverse
- Statement version
- 2
- SHA-256
- c8c917ac4451a862e674bea3c2f5a0f02f73b819ccf8c4aad831370b098f0aac