Skip to content

About

Computer-assisted proofs and clean-room audits for the r=10 and r=11 fixed cases of Erdős Problem 617.

Topics

Resources

Contributing

Stars

0 stars

Watchers

0 watching

Forks

Latest commit

 

History

2 Commits

Folders and files

Repository files navigation

The fixed cases r=10 and r=11 of Erdős Problem 617

Pre-review v0.1.1 artifact release — not externally peer reviewed or proof-assistant formalized.

This repository contains computer-assisted proofs of two fixed cases of the Erdős–Gyárfás balanced-colouring conjecture:

  • Every 10-edge-colouring of K_101 contains 11 vertices whose induced complete graph omits a colour.
  • Every 11-edge-colouring of K_122 contains 12 vertices whose induced complete graph omits a colour.

The general all-r conjecture remains open.

Authorship and direction

AI-authored; directed by Adam Lee Terpstra, Independent researcher, and prepared for human submission.

OpenAI Codex materially generated the mathematical arguments, computational classifications, verifier code, adversarial checks, and exposition. Adam Lee Terpstra selected and directed the project, made continuation and verification decisions, required separate clean-room audits, and serves as submitter and artifact custodian. See AI_USAGE.md for the full disclosure.

Verification status

Both results were assessed as valid in separate clean-room computational audits. They are not Lean-formalized, backed by LRAT certificates, externally peer reviewed, or independently proved by a human mathematician.

  • r=10: the audit independently regenerated the critical finite families, checked 4,923,214 inherited-density subsets and 4,987,794 row-cover partitions, and replayed all 48 outer comparisons. The last margin is one.
  • r=11: 33 independently written files were frozen before comparison with submitted code; all 31 post-freeze comparison runs passed. The decisive contextual comparison is 287 against a budget of 286.

The final publication-directory replay found one executable defect in a frozen r=11 audit script: an impossible cover-size-four bipartition had not been filtered. The submitted derivation and verifier contained the necessary condition; the documented release repair reproduces maxima 19 and 25. See RELEASE_REPLAY_NOTE.md. This does not currently indicate a theorem-level gap, but it narrows the clean-room executable claim and is disclosed for expert review.

Every issue found during the two clean-room audits and the final release replay is itemized in REVIEW_DISPOSITION.md, with its severity, correction, and current status. No known theorem-level defect is unresolved. Historical source and logs that contain superseded errors are retained and labeled for provenance; the public replay uses the corrected paths.

See CLAIMS.md for the exact claims and non-claims.

Licensing

Original code and computational artifacts are offered under Apache-2.0. The paper is offered under CC BY 4.0 to the extent applicable. Third-party material retains its original terms.

Repository map

  • paper/: current combined-paper draft and the inspected r=10 audit PDF.
  • proof/r11_submission/: the 295 non-bytecode files from the submission audited for the r=11 theorem. The full 401-row audited manifest is retained; 106 generated .pyc cache files were omitted from the public tree because some embed absolute local paths.
  • audits/r10/: independent r=10 audit, manuscript, certificates, and replay.
  • audits/r11/: independent r=11 audit, implementations, logs, and replay.
  • REPRODUCE.md: entry points and expected runtimes.
  • PUBLICATION_REDACTIONS.md: exact local-path redactions and before/after hashes.
  • RELEASE_REPLAY_NOTE.md: a frozen-audit replay defect and its public repair.
  • REVIEW_DISPOSITION.md: consolidated finding-by-finding correction ledger.
  • COMPUTE_ACCOUNTING.md: scoped token, elapsed-time, and API-equivalent-cost accounting for the research task and two independent audits.
  • FINAL_REPLAY.md: publication-directory validation performed before the initial public release.

Release status

All public-directory computational steps passed on 11 August 2026 after the two replay-packaging repairs documented in RELEASE_REPLAY_NOTE.md. The r=10 replay passed as one clean run; the r=11 release checks passed in a segmented final run while the two defects were found and corrected. See FINAL_REPLAY.md for the exact scope.

The combined conventional paper remains in preparation; the Markdown file in paper/ is a technical draft, not a finished manuscript. Corrections and independent checks are explicitly invited through GitHub Issues or by email at terpstra.research@gmail.com.

About

Computer-assisted proofs and clean-room audits for the r=10 and r=11 fixed cases of Erdős Problem 617.

Topics

Resources

Contributing

Stars

0 stars

Watchers

0 watching

Forks

Releases

Packages

Contributors

Languages