AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

An explicit noncoordinate polynomial with affine three-space zero fibre

Does the classical conjecture or property hold, or does there exist a counterexample as established in An explicit noncoordinate polynomial with affine three-space zero fibre?

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 049)

Model / AI: OpenAI (unreleased)

machine-checked (formal proof)self-reported (formal proof)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'An explicit noncoordinate polynomial with affine three-space zero fibre'. We construct an explicit counterexample to the Abhyankar–Sathaye conjecture: a noncoordinate polynomial in four complex variables whose zero fibre is affine three-space. Adjoining variables gives counterexamples in every ambient dimension at least four.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 049). The Lean development was not rebuilt locally.