Wall's D(2) problem

Wall's D(2) problem asks whether every finite CW complex satisfying Wall's D(2) condition is homotopy equivalent to a finite complex of dimension at most two. A manuscript in OpenAI's public mathematics collection (github.com/openai/math), dated 6 October 2026, claims a counterexample. This page summarizes the published claim 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:
  • For a finite connected CW complex X with fundamental group G and universal cover X̃, the D(2) condition asks that H_i(X̃; Z) = 0 for i > 2 and H³(X; M) = 0 for every ZG-module M. Wall introduced it in 1965, and the problem appears as Problem D3 in his 1979 list. No asphericity hypothesis is imposed.
  • A stable version has a positive answer: adding enough two-spheres makes a finite D(2) complex homotopy equivalent to a finite two-dimensional complex (Cohen; Hambleton bounds the number of spheres).
  • Positive results for particular fundamental groups include Hambleton's theorem for the finite subgroups of SO(3) and work of Hofmann and Nicholson on generalized quaternion groups of orders 24 and 32, which shows that the long-standing candidate of Cohen and Dyer has a finite two-dimensional model.
  • Bridson and Tweedale constructed finite D(2) complexes with virtually free fundamental groups whose failure to have two-dimensional models was conditional on a relation-gap assertion.

The original result

• Claim. Theorem 1.1 of A Counterexample to Wall's D(2) Problem states that there is a finite connected three-dimensional CW complex X satisfying the D(2) condition that is not homotopy equivalent to any finite CW complex of dimension at most two. Its fundamental group is infinite.
• Method, as described:
  • An obstruction: on a finite two-dimensional complex Y, if the second homology with coefficients in a rank-one complex local system given by a character ρ vanishes, then ρ is trivial on every element of finite order. The proof uses a tower of infinite cyclic covers following Howie's cyclic-tower method.
  • A construction: a five-generator, four-relator presentation with a perfect normal subgroup normally generated by two powers. The quotient has an element of order two detected by a complex character, and an exact boundary calculation shows that the twisted second homology of the presentation complex vanishes. Quillen's plus construction, in Mannan's finite form, then gives the finite D(2) complex.
• Source. The manuscript A Counterexample to Wall's D(2) Problem at commit 1581d4c.
• Formalization. The repository's Lean documentation at commit 1581d4c has no scope note for this manuscript.

Public follow-up work

Date	Work	Relation	Public claim	Public status (checked 19 October 2026)
2026-10-13	chlee-0/formalization_relation_gap_problem (GitHub, commit 283943b)	Extension (Lean)	The README describes a Lean 4 formalization, using Mathlib, of a relation gap and of global deficiency zero for the group of the manuscript. For the specified quotient map from the free group on five generators with kernel N, it states that the relation module of N needs four generators as a module over the group ring while N needs five normal generators, and that every finite presentation of the group has deficiency at most zero. It states that neither result is stated in the original manuscript, that the formalization was carried out primarily by the AI models Claude Opus 5.5 and GPT-6.1 Sol, and that it does not formalize the manuscript's complete proof of the D(2) counterexample.	GitHub repository.
2026-10-14	Pyronis, Inc., Pyronis-Inc/WallD2 (GitHub, commit 5c01b38)	Formalization (conditional Lean)	The README describes a conditional Lean formalization of the counterexample. The algebraic layers, including the perfectness of the normal subgroup and the element of order two, are proved, and the topological inputs enter as named axioms: plus_assembly for Mannan's finite plus construction and howie_tower for the tower obstruction. Its recorded axiom report for the composed theorem lists these named axioms besides the standard ones.	GitHub repository.
2026-10-16	J. Jardine, Lattice24, referee review rank_483 in JJardine919/openai-math-audit (archived at Zenodo 10.5281/zenodo.23422995)	Review (AI-assisted audit)	Reports no gap, with no minor notes. The reviewer states that it read all four sections in full and checked the tower obstruction step by step, including the specialization of the twisted boundary determinant and the strict increase of simplex counts along the tower.	Part of an audit of the collection's manuscripts without Lean that the audit describes as complete. The reviews are published under CC BY 4.0.
2026-10-16	L. Bartholdi, M. R. Bridson, R. Mikhailov, J. Nicholson, Two-generator presentations with a relation gap (arXiv:2610.23637, v1)	Parallel (relation gap) and use (D(2), conditional)	For coprime p, q ≥ 2, the paper shows that the presentation ⟨x, t | xpq, [xp, txqt−1]⟩ has a cyclic relation module but does not present a one-relator group, and states that this settles the relation gap problem. It describes these examples as related to the manuscript but says its proof is elementary and completely independent of that work. Attaching a single three-cell to each presentation complex gives counterexamples to Wall's D(2) problem with six cells. The paper states that this corollary relies on Corollary 2.3 of the manuscript and can be regarded as conditional on it. Its declaration of AI usage states that ChatGPT 6 Astra assisted with the discovery of the groups and the proof, and that Claude Fable 5.1 was consulted.	arXiv preprint (version 1 only).

Notes

• The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.