What was already known
Dittert’s inequality is a recognized matrix problem. A separate exact dimension-five proof bundle predates this candidate.
AI involvement
GPT-5.6 Sol selected the problem and generated the certificate, verification code and Lean files. Arthur Moisés da Costa Borges maintained the release and says he did not independently validate the mathematics.
The cited provenance says the model carried out the mathematical search and certificate work with minimal human mathematical supervision.
Importance
The candidate supplies a separate machine-checkable route for dimension five, subject to validation of its mathematical encoding.
Limitations
No qualified human has validated the encoding against the original statement. The earlier independent proof does not check this certificate.
Technical verification
Lean and exact Python/FLINT checks reportedly verify the encoded certificate, but no qualified human has validated the encoding or correspondence to Dittert’s original statement. Thus complete verification of the natural-language claim is not established.
Independent checking
Lean theorem compilation and independent-from-recovery exact certificate checking
- Checker
- Lean 4 with Mathlib, including native_decide; separate Python/FLINT verifier
- Scope
- Encoded n=5 bound and equality certificate with 54 orbital identities, 425 kernel constraints and positivity checks
- Basis
- Reported by the linked checker
Human understanding
The human custodian expressly reports not understanding the central mathematics. No later human explanation of this artifact was found.
Correction and publication history
The candidate supplies a separate machine-checkable route for dimension five, subject to validation of its mathematical encoding.
Read this published revision