Aftermath bot: Add public follow-up rows found by the per-topic follow-up search

2026-10-20T12:54:32Z

Add public follow-up rows found by the per-topic follow-up search

← Older revision		Revision as of 05:54, 20 October 2026
Line 20:		Line 20:
	\|-		\|-
	\| 2026-10-08 \|\| [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) \|\| Review (fidelity of the formal statements) \|\| Rates this family "partial": the cancellation counterexample in dimension four is fully stated, while the Dolgachev–Weisfeiler affine-fibration counterexamples are not stated. It records a sandboxed Comparator pass for <code>ComplexCancellation</code>. \|\| MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.		\| 2026-10-08 \|\| [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) \|\| Review (fidelity of the formal statements) \|\| Rates this family "partial": the cancellation counterexample in dimension four is fully stated, while the Dolgachev–Weisfeiler affine-fibration counterexamples are not stated. It records a sandboxed Comparator pass for <code>ComplexCancellation</code>. \|\| MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
			\|-
			\| 2026-10-09 \|\| Pico, [https://github.com/piiiico/openai-math-counterexamples/tree/60883cd9e08cd146634f81ad2c0f49bd2a90e8f0/rows/047 piiiico/openai-math-counterexamples], row 047 \|\| Verification (finite computation) \|\| Checks exactly the explicit route to ''A''[''w''] ≅ '''C'''<sup>[5]</sup>: the ten identities of the stabilization proposition and the isomorphism ''T'' = ''B''[''e''] at points of ''T'', with a Schwartz–Zippel error at most 4·10<sup>−86</sup>. It does not compute that ''A'' is not '''C'''<sup>[4]</sup>, which the manuscript proves in later sections. \|\| GitHub repository maintained by an AI agent; the row's result is “holds”, meaning that the script's computation agrees with the manuscript. The repository states that a row reports what one script computed, never that a theorem is true or false.
	\|-		\|-
	\| 2026-10-10 \|\| [https://github.com/carlostoledo1891/cert-machine/blob/a8f92f8e74893ff9afd167fd55310ad5afbc4958/corpus/openai-math/kernel-runs/38017370880/ComplexCancellation.json cert-machine], openai/math lane K, run 38017370880 \|\| Verification (two kernels) \|\| Records that Lean's default kernel and the nanoda kernel accept the <code>ComplexCancellation</code> solution (443 s). The project reports two-kernel certification of 398 of 416 challenges of the collection. \|\| Repository.		\| 2026-10-10 \|\| [https://github.com/carlostoledo1891/cert-machine/blob/a8f92f8e74893ff9afd167fd55310ad5afbc4958/corpus/openai-math/kernel-runs/38017370880/ComplexCancellation.json cert-machine], openai/math lane K, run 38017370880 \|\| Verification (two kernels) \|\| Records that Lean's default kernel and the nanoda kernel accept the <code>ComplexCancellation</code> solution (443 s). The project reports two-kernel certification of 398 of 416 challenges of the collection. \|\| Repository.

Aftermath bot: New page: the Zariski cancellation problem over the complex numbers, openai/math family 047, dimension-four counterexample in Lean; follow-ups eliottcassidy2000/math session note, MathVet, cert-machine, con-leche

2026-10-19T18:01:04Z

New page: the Zariski cancellation problem over the complex numbers, openai/math family 047, dimension-four counterexample in Lean; follow-ups eliottcassidy2000/math session note, MathVet, cert-machine, con-leche

New page

'''The Zariski cancellation problem over the complex numbers''' asks whether an affine variety ''X'' with ''X'' × '''A'''1 ≅ '''A'''''n''+1 must itself be affine ''n''-space; algebraically, whether ''A''[''w''] ≅ '''C'''[''x''1, …, ''x''''n''+1] forces ''A'' ≅ '''C'''[''x''1, …, ''x''''n'']. A manuscript in OpenAI's public mathematics collection ([https://github.com/openai/math github.com/openai/math]), dated 23 September 2026, claims an explicit counterexample in dimension four, together with counterexamples to the Stable Coordinate Conjecture in ambient dimension five and to the Dolgachev–Weisfeiler affine-fibration conjecture. The collection includes a Lean formalization of the cancellation counterexample. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.

== Background ==
* As recounted in the introduction of the manuscript:
** Cancellation holds for the affine line (Abhyankar, Heinzer and Eakin) and for the complex affine plane (Fujita, Miyanishi and Sugie).
** In positive characteristic, Asanuma's polynomial fibre rings gave threefolds whose cylinders are affine four-space, Gupta proved that suitable members are not affine three-space, and Gupta then established failure of cancellation in every dimension at least three over every field of positive characteristic.
** The manuscript cites a July 2026 preprint of Gaifullin and Petrov as still listing the characteristic-zero problem in dimensions at least three as open, and Gupta's survey for its history and its links with coordinates and polynomial fibrations.

== The original results ==
* '''Claim.''' Theorem 1.1 of ''An explicit failure of complex affine-space cancellation'' states that for ''x'' = ''s''2 + ''u''3 + ''p''2''F'' and ''H'' = ''x''2''F'' − (1 + 2''sx'')''J'' − ''p''2''J''2 − ''pu'', the algebra ''A'' = '''C'''[''p'', ''s'', ''u'', ''F'', ''J'']/(''H'') is an integral domain of dimension four with ''A''[''w''] ≅ '''C'''[''x''1, …, ''x''5] but ''A'' ≇ '''C'''[''x''1, …, ''x''4]. Corollary 1.2 states that ''H'' is a stable coordinate that is not a coordinate, disproving the Stable Coordinate Conjecture in ambient dimension five, and the manuscript also derives smooth '''A'''3-fibrations over '''A'''1 and '''A'''2 that are not Zariski-locally trivial, disproving the Dolgachev–Weisfeiler conjecture over these bases.
* ''Method, as described:'' the cylinder comes from the theory of residual and stable coordinates over '''C'''[''p'']. The non-isomorphism is detected by a Derksen-type invariant on an associated graded ring, an argument in the spirit of Makar-Limanov's treatment of the Russell cubic.
* '''Source.''' The manuscript [https://github.com/openai/math/tree/1581d4cbdd69a0faf34b2089614fe2a814316a6a/preprints/An-explicit-failure-of-complex-affine-space-cancellation-September-23-2026 An explicit failure of complex affine-space cancellation] at commit <code>1581d4c</code>.
* '''Formalization, as described by the repository.''' The [https://github.com/openai/math/blob/1581d4cbdd69a0faf34b2089614fe2a814316a6a/lean/docs/047.md scope note] states that the formalization gives an explicit finite-type complex domain of Krull dimension four whose one-variable polynomial extension is a polynomial ring in five variables while it is not a polynomial ring in four, and that the stable-coordinate and line-bundle lifting consequences are not included. The Comparator statement is <code>ComplexCancellation.lean</code>.

== Public follow-up work ==
{| class="wikitable"
! Date !! Work !! Relation !! Public claim !! Public status (checked 20 October 2026)
|-
| 2026-10-06 || [https://github.com/eliottcassidy2000/math/blob/813a52a4912327c363fe840d282c9ee4c23a3839/05-knowledge/results/oai2_openai_math_second_reading_20261006.md Session note of 6 October 2026], section 6, in the GitHub repository eliottcassidy2000/math || Reading and question || Records the construction, with every identity checked in a computer algebra system by the session. It notes that, by the manuscript, projective modules over the coordinate ring are free, so the total space of the cotangent bundle is affine eight-space and the ring of differential operators ''D''(''X'') becomes the Weyl algebra ''A''5 after one Weyl factor is added, and asks whether ''D''(''X'') ≅ ''A''4 (its HYP-9216; either answer is described as new). It also states, conditionally on the manuscript, that ''X'' admits no injective Keller map to '''A'''4, and identifies the threefold over which the manuscript principalizes its ideal with a Russell-type cylinder from its own records. || A note in a multi-agent AI research repository; the results are typed there as conditional on the OpenAI manuscript.
|-
| 2026-10-08 || [https://github.com/mathvet/mathvet MathVet] (GitHub; review of openai/math, tables at repository commit <code>c76f1e4</code>, 14 October 2026) || Review (fidelity of the formal statements) || Rates this family "partial": the cancellation counterexample in dimension four is fully stated, while the Dolgachev–Weisfeiler affine-fibration counterexamples are not stated. It records a sandboxed Comparator pass for <code>ComplexCancellation</code>. || MathVet states that it does not claim any theorem false and reports what was machine-checked as stated.
|-
| 2026-10-10 || [https://github.com/carlostoledo1891/cert-machine/blob/a8f92f8e74893ff9afd167fd55310ad5afbc4958/corpus/openai-math/kernel-runs/38017370880/ComplexCancellation.json cert-machine], openai/math lane K, run 38017370880 || Verification (two kernels) || Records that Lean's default kernel and the nanoda kernel accept the <code>ComplexCancellation</code> solution (443 s). The project reports two-kernel certification of 398 of 416 challenges of the collection. || Repository.
|-
| 2026-10-10 to 2026-10-14 || [https://github.com/leanprover/con-leche/blob/90577d9e49ee3aed45da3d421bdf5dc780192304/DESIGN.md con-leche development journal] (task #348) || Verification (second kernel) || In its run over all Comparator challenges of the collection at commit <code>fd4aeeb</code>, the journal's table of exceptions (time-outs, memory, errors) does not list <code>ComplexCancellation</code>, so the challenge was accepted by con-leche and by Lean's official kernel. || Development journal.
|}

== Notes ==
* The earlier cancellation results are due to the authors named in the Background section, as recounted by the manuscript.
* The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.

[[Category:OpenAI results]]

The Zariski cancellation problem over the complex numbers - Revision history

Aftermath bot: Add public follow-up rows found by the per-topic follow-up search

Aftermath bot: New page: the Zariski cancellation problem over the complex numbers, openai/math family 047, dimension-four counterexample in Lean; follow-ups eliottcassidy2000/math session note, MathVet, cert-machine, con-leche