Dittert's Conjecture in Dimension Five
The dimension-five case asks whether, for every nonnegative real matrix whose entries sum to , the Dittert functional is uniquely maximized at . The submitted artifact claims the stronger quantitative bound which implies uniqueness.
- Result
- Proved(see note)
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Computation
- Field
- Linear algebra; permanents; exact sum-of-squares certificates
- Posed by
- Eberhard Dittert
- Year posed
- 1983
- Years open
- 43y
- Solved
- 2026-08-06
- Model
- GPT-5.6 Sol (Ultra)
- Vendor
- OpenAI
- Collaborators
- Arthur Moisés da Costa Borges
- Verification
- Lean-checked, statement unaudited
- Publication
- Announced
- Significance
- 15 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What was actually shown
Dimension 5 only; public AI-generated candidate with no independent specialist review.
What the AI did
Operating through OpenAI Codex, GPT-5.6 Sol with the Ultra reasoning-effort setting selected the problem after literature triage, developed the symmetry-reduced sum-of-squares approach, ran numerical discovery and rational recovery, produced the exact certificate and mechanically separate verifier, formalized the quantitative bound and equality characterization in Lean 4, audited the artifacts, and wrote the manuscript. Human mathematical supervision was minimal. Arthur Moisés da Costa Borges defined the broad objective, authorized execution and publication decisions, supplied factual metadata, and maintains the artifact, but did not derive or independently validate its technical content.
Verification
The public artifact contains a Lean 4.30.0-rc1 formalization of the n=5 quantitative bound and equality characterization, with no sorry, admit, or user-declared axioms. Lean checks the included exact rational SOS witness directly. Large finite equalities use native_decide; the trusted base therefore includes Lean's native compiler and runtime, not the kernel alone. A separate Python/FLINT verifier checks 54/54 orbital identities, 425/425 kernel constraints, and 420/420 positive leading principal minors; deterministic generators reproduce the PSD witness and 41 Lean data modules. No independent specialist has yet checked the informal-to-formal correspondence, historical or novelty claims, or the overall argument. Treat this as a public AI-generated candidate, not an established or peer-reviewed result. Tier: the same system produced both the proof and its Lean formalization, and no independent party has audited the informal-to-formal correspondence.
Source
Submitted by LuckyMongoose479 on