# An AI-Generated Candidate for Dittert's Conjecture in Dimension Five

This repository contains an AI-generated, machine-checked candidate based on
an exact symmetry-reduced sum-of-squares certificate and a Lean formalization
for Dittert's conjecture in dimension five. No qualified human specialist has
independently validated the mathematics, the formal specification, or the
claimed novelty. This artifact must not be cited as an established solution.

If the mathematical encoding and the paper-to-artifact correspondence are
correct, the certificate establishes, for every nonnegative real
\(5\times5\) matrix \(A\) whose entries sum to \(5\),

\[
\Phi(A)\leq \frac{1226}{625}
-\frac{\lVert A-U_5\rVert_F^2}{625},
\]

where \(U_5=J_5/5\) and

\[
\Phi(A)=\prod_i r_i+\prod_j c_j-\operatorname{per}(A).
\]

The resulting candidate conclusion is that the maximum \(1226/625\) is
attained if and only if \(A=U_5\).

> **Status:** public research artifact, version label
> `0.1.0-public-candidate`, 6 August 2026. It was generated by AI with minimal
> human mathematical supervision and released on GitHub for inspection,
> reproduction, criticism, and further research. It has not been reviewed by a
> qualified specialist, deposited as a formal preprint, or submitted to a
> journal, and must not be described as an established or accepted result.

## Human contributor and artifact custodian

Arthur Moisés da Costa Borges<br>
Independent Researcher, Brazil<br>
[arthurborges.dev@gmail.com](mailto:arthurborges.dev@gmail.com)

Arthur initiated the broader open-mathematics experiment, specified workflow
preferences, authorized tool execution and publication decisions, supplied
factual metadata, and maintains the artifact. He did not derive, understand,
or independently validate the mathematical and formal content.

## AI provenance and roles

The principal model was GPT-5.6 Sol with the Ultra reasoning-effort setting,
operated through the OpenAI Codex agentic harness. The AI system performed or
coordinated the problem selection, literature triage, mathematical search,
certificate recovery, verification code, Lean formalization, internal audits,
and manuscript preparation. AI systems are not authors.

The complete allocation of roles and the remaining validation gap are recorded
in [`manuscrito/PROVENIENCIA-IA.md`](manuscrito/PROVENIENCIA-IA.md).

## Repository structure

- `certificados/`: exact rational certificate and compact PSD witness;
- `formal/`: Lean 4 formalization and generated certificate data;
- `manuscrito/`: candidate manuscript and expert-review package;
- `pesquisa/`: research log and mathematical audits;
- `scripts/`: discovery, recovery, generation, and verification programs;
- `tests/`: Python unit tests;
- `vibemath/`: exact polynomial and symmetry infrastructure;
- `resultados/`: numerical discovery outputs, which are not used as proof.

## Mechanically separate exact verification

Python 3.12 and `python-flint` 0.9.0 were used for a mechanically separate
software-verification path. It is separate from the recovery code; it is not
independent human review. The verification pipeline was produced and operated
within the same AI-led workflow.

```bash
python3.12 -m venv .venv
.venv/bin/python -m pip install -r requirements-verification.txt
.venv/bin/python scripts/verify_n5_exact_certificate.py
python3 -S scripts/generate_n5_lean_witness.py --check
python3 -S scripts/generate_n5_lean_certificate_data.py --check
python3 -m unittest discover -v
```

Expected checks:

- 54 of 54 orbital coefficient identities;
- 425 of 425 kernel constraints;
- 420 of 420 positive leading principal minors;
- five PSD-witness blocks and 420 nonnegative SDD margins;
- 41 deterministically regenerated Lean data files;
- 22 of 22 Python tests.

The detailed commands, expected hashes, and reviewer checklist are in
[`manuscrito/PACOTE-DE-REVISAO.md`](manuscrito/PACOTE-DE-REVISAO.md).

## Lean verification

The formalization is documented in
[`formal/README.md`](formal/README.md) (Portuguese) and
[`formal/README.en.md`](formal/README.en.md) (English).

The project pins Lean and Mathlib to `v4.30.0-rc1`.

```bash
cd formal
lake exe cache get
lake build Dittert5
lake env lean Dittert5/AxiomAudit.lean
```

The candidate's final Lean theorems are:

```lean
Dittert5.dittert_dimension_five_bound
Dittert5.dittert_dimension_five_equality_iff
```

### Trust boundary

The Lean sources contain no `sorry`, `admit`, or user-declared `axiom`
command, but the formal route within the encoded specification is not
kernel-only. Large finite checks use
`native_decide`. The executable normalizer and SOS evaluator are the actual
logical definitions, and kernel-checked lemmas prove that their operations
preserve polynomial evaluation; no local `implemented_by` override is used.
The global native check compares the canonical certificate with an aggregated
118,755-key target map whose equivalence to the original target is proved in
the kernel.
The trusted base therefore includes the Lean native compiler and runtime as
well as the kernel. The standalone Python/FLINT verifier is independent of the
recovery code, but does not remove this formal trust boundary.

## Citation

Candidate citation metadata are provided in [`CITATION.cff`](CITATION.cff).
The public repository is
[`arthurborgesdev/dittert-conjecture-n5`](https://github.com/arthurborgesdev/dittert-conjecture-n5);
until an immutable tag or release exists, readers should identify the exact
Git commit they inspect or cite. Public availability enables scrutiny but does
not constitute expert validation or peer review. arXiv and DOI fields must not
be added before real records exist. Planning documents for any later formal
submission are in
[`manuscrito/ARXIV-SUBMISSAO.md`](manuscrito/ARXIV-SUBMISSAO.md) and
[`manuscrito/AFM-SUBMISSAO.md`](manuscrito/AFM-SUBMISSAO.md). Qualified
technical scrutiny is invited through
[`manuscrito/REVISAO-ESPECIALISTA.md`](manuscrito/REVISAO-ESPECIALISTA.md);
the separate factual and authorization record for the human custodian is
[`manuscrito/REVISAO-DO-AUTOR.md`](manuscrito/REVISAO-DO-AUTOR.md).

## Licensing

The article and research documentation use CC BY 4.0, original source code
uses the Zero-Clause BSD License, and certificate/data artifacts use CC0 1.0.
See [`LICENSE.md`](LICENSE.md) for the precise file scopes and
[`formal/PROVENANCE.md`](formal/PROVENANCE.md) for the clean-room and
source-similarity record.

The `aviso` embedded in the frozen rational-certificate JSON records the
artifact's pre-formalization state. It is retained byte for byte for hash
reproducibility; the current status is the machine-audited Lean candidate
described above, still awaiting independent human mathematical validation.