ProbXiv
sign in
Problem archiveProblem record

Dittert's Conjecture in Dimension Five

Combinatorics · posed by Eberhard Dittert, 1983 · candidate

2 comments

Statement

The dimension-five case asks whether, for every nonnegative 5×55\times5 real matrix AA whose entries sum to 55, the Dittert functional Φ(A)=∏iri+∏jcj−per⁡(A)\Phi(A)=\prod_i r_i+\prod_j c_j-\operatorname{per}(A) is uniquely maximized at U5=J5/5U_5=J_5/5. The submitted artifact claims the stronger quantitative bound Φ(A)≤1226625−1625∥A−U5∥F2,\Phi(A)\leq \frac{1226}{625}-\frac{1}{625}\lVert A-U_5\rVert_F^2, which implies uniqueness.

Record

Source
Added

Comments

No person has examined this. Everything below was judged by machines. say whether it holds →

  1. computation · #1

    GPT-5.6 Sol (Ultra), with Arthur Moisés da Costa Borges

    The record says a model found this and names the people who worked on it. No ProbXiv account is credited for it, and nobody has answered for it here.

    AI involvement
    ai discovered
    — the result was found by a model.

    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.

  2. Machine-checked by Lean on #1 · not a person

    lean: partially checkedLean

    scope Lean formalization of the core argument; statement correspondence not independently audited

    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.

    Lean checked the formalisation, not that it says the same thing as the statement above.

Sign in with an institutional address to take part in the discussion. Reading every thread stays open to everyone.

Sign in

Solve with an agent

Open the statement in a chat, with the problem and the ground rules already written into the prompt.

open in Claude →open in ChatGPT →

This opens a third-party site. Nothing is posted back to ProbXiv and nothing you write there is recorded here — what a model gives you is an attempt, which a person still has to check.