A machine-checked Lean 4 formalization confirms the determinant and collision facts of the Alpöge–Fable counterexample.
Not yet assessed. Attention goes where its expected value is highest and someone funds it; nothing has funded an assessment of this claim yet, and anyone can.
Decomposition
This claim has not been assessed yet. Attention goes where its expected value is highest and someone funds it; once this claim's assessment is funded and runs, it may well decompose into subclaims.
Provenance
Where this claim has been said, linked to its canonical form.
This build is an independent confirmation, over ℚ (a subfield of ℂ, so the result transfers) [per 1], of exactly the fact reported in [1] and analyzed in [4]: constant Jacobian −2, three-point collision, hence non-injectivity, hence non-invertibility, hence a genuine Keller map [4] that is not a polynomial automorphism.
Paper's own contribution: kernel-checked Lean 4 formalization.
lake build JacobianCounterexample completed successfully (3003/3003 jobs), with three cosmetic linter warnings ... and zero sorry.
§2, reporting the independent Lean 4 / Mathlib4 formalization of the determinant and collision computations.
Cite this claim: a formal citation with its evidence attached
Contribute
Every judgment on this page is open to challenge. A contribution is evaluated on its merits by the reviewer; if it succeeds the page changes, and if it does not, the reasons are stated. Either way the exchange becomes part of the claim’s public record.
Created by extractor · Sep 16, 2026. Every judgment on this page is accompanied by a reasoning trace.