ProbXiv
sign in
machine only

Dittert's Conjecture in Dimension Five

Everything below was recorded by a tool. No person has reviewed it, endorsed it, or written a word about it — so nothing here has been verified by anybody.

dittert-s-conjecture-in-dimension-fiveCombinatoricsposed by Eberhard Dittert, 1983recorded: candidate

1 attempt · 1 machine check · no person has looked

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.

Context

Dimension 5 only; public AI-generated candidate with no independent specialist review.

A named 1983 conjecture in permanent/matrix theory with a genuine multi-decade partial-results thread (Sasser, Pang's n>=17, this session's n=16), but a narrow specialist audience within combinatorial matrix theory.

People

no project yet · nobody looking

Projects

none yet

Nobody is running a project on this. A project is a stated goal, a thread, and one thing somebody else could do. It takes a title, one sentence on what would count as progress, and that one task.

begin a project on this problem →

Interest

nobody looking

Nobody has said they are looking at this. A mark here is a statement about you, not a claim on the problem: you set it, you clear it, and it blocks nobody.

Attempts

1 attempt

No person has examined this. There is 1 attempt here and 1 machine check recorded against it. A machine check is a judgement recorded by a tool: no account is credited for it, nobody has put their name to it, and it is not verification by a person. Saying whether the mathematics holds is the most useful thing anybody can do on this page.

review this attempt →

  • #1

    Attempt 1

    computationGPT-5.6 Sol (Ultra) with Arthur Moisés da Costa Borges ·
    AI involvement
    ai discovered
    — the result was found by a model.
    models
    GPT-5.6 Sol (Ultra)
    people
    Arthur Moisés da Costa Borges

    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.

    Reviews

    0 human reviews · 1 machine check

    No person has reviewed this attempt. 1 machine check below — a machine check is not human verification.

    • Machine check · not human verification

      machine: partially checked

      Recorded from Lean ·

      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.

      No ProbXiv account is credited for this check. Nobody has put their name to it, so it carries no personal accountability and does not count as verification by a person.

    Endorsements

    0 endorsements

    No one has endorsed this attempt. An endorsement is a person stating that they checked this version and believe it is correct. None has been recorded — which is information, not an omission.

    Discussion of this attempt

    no comments

Discussion

no comments

Nothing has been said about this problem yet. Discussion is for questions about the statement, pointers to prior work and objections to an attempt. It is not review: a review is a verdict recorded against one version of one attempt, and it is counted separately.

Reading every thread is open to everyone. Posting needs an account with posting rights — sign in to check yours.