The source proves constant formal polynomial Jacobian determinant, a three-point fiber, and failure of a polynomial inverse for the recorded Jacobian conjecture statement.
Public formal source; build and independent mathematical review are separate checks.
1 cited passage ↓1 problem ↓Record b8eec94711a9b73151929b78cbd7cb999a008590 ↓
The exact passages cited in OpenMath. Each passage identifies how its wording was recorded.
The source proves constant formal polynomial Jacobian determinant, a three-point fiber, and failure of a polynomial inverse for the recorded Jacobian conjecture statement.
Passage ID: jacobian-conjecture:entry:lean:v1
Source item: lean
Source record: jacobian-conjecture:source:lean:v1
Explicit citations in versioned problem publications. A citation records a use; it does not confer proof or independent verification.
Problem publication v8
Source assessment
Proved
Formal polynomial counterexample reported complete
The pinned algebraic statements, not an analytic derivative identification.
Observed Oct 13, 2026
Construction
Exact polynomial map and repeated fiber
Formal declaration
Lean: the three-point fiber
Source assessment
Proved
Formal polynomial counterexample reported complete
The pinned algebraic statements, not an analytic derivative identification.
Observed Oct 13, 2026
Formal declaration
Lean: no polynomial inverse for the rational witness
Research activity
Formal algebraic evidence
The pinned Lean project supplies separately inspectable determinant, collision and no-inverse statements.
No OpenMath build or independent proof adjudication has been performed.
History
Polynomial counterexample formalized
Question
Jacobian conjecture
Further reading
Inspect the formal statement, assumptions and reported checks.
Linked manuscripts, code and data. External proof reports, statement correspondence and OpenMath execution are separate checks.
Formal code
No OpenMath execution recorded
Public source inspected for statement and assumptions; this proof project has not been executed by OpenMath.
Resource revision: b8eec94711a9b73151929b78cbd7cb999a008590
Complete formal proof reported externally
The polynomial witness is source-reported complete; OpenMath has not built it. The project also proves jacobian_det and not_injective.
Statement match: Linked by OpenMath · independent review separate · checked Oct 13, 2026
Alpoge.three_point_fiberCommit b8eec94711a9b73151929b78cbd7cb999a008590
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
Alpoge.FormalConjecturesJC.jacobian_conjecture_falseCommit b8eec94711a9b73151929b78cbd7cb999a008590
Recorded authorship
alerad/alpoge-lean project
The project reports an AI-assisted formalization and computer-algebra workflow; this is distinct from the original discovery.
OpenMath source records preserve exact citations. Observation dates order these records; they do not establish the latest upstream paper or proof.
Alpöge counterexample in Lean
OpenMath supplies original paraphrases and links; no proof text is republished.
Source terms ↗