AWESOME AI PROOFS
← Problems
Research / Oct 6, 2026

A Counterexample to the Group-Ring Determinant Conjecture

Does the classical conjecture or property hold, or does there exist a counterexample as established in A Counterexample to the Group-Ring Determinant Conjecture?

Model / AI: OpenAI (unreleased)

machine-checked (counterexample)self-reported (counterexample)
Oct 6, 2026

Lean formalization in OpenAI math repository (Result 197)

Model / AI: OpenAI (unreleased)

machine-checked (counterexample)self-reported (counterexample)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'A Counterexample to the Group-Ring Determinant Conjecture'. We disprove the unrestricted group-ring Determinant Conjecture. We construct a finitely generated group G and a square matrix over \mathbb Z[G] that is invertible over \mathbb Q[G] and has Fuglede–Kadison determinant strictly between zero and one. The logarithmic integral defining the determinant is finite.

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