VibeMathed reports this item as candidate. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
The dimension-five case asks whether, for every nonnegative $5\times5$ real matrix $A$ whose entries sum to $5$, the Dittert functional $\Phi(A)=\prod_i r_i+\prod_j c_j-\operatorname{per}(A)$ is uniquely maximized at $U_5=J_5/5$. The submitted artifact claims the stronger quantitative bound $$\Phi(A)\leq \frac{1226}{625}-\frac{1}{625}\lVert A-U_5\rVert_F^2,$$ which implies uniqueness.
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement
fidelity, correctness, priority, or novelty.
What AI did
GPT-5.6 Sol (Ultra)
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.
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.