u/EqualFit7779 — reddlx

I’m releasing a GPT-5.5 Pro-assisted proof-candidate package for Graham’s rearrangement conjecture, also listed as Erdős Problem #475.

Repo:
https://github.com/Atomicium-org/graham-rearrangement-certificates

Some context, because the status of this problem is subtle:

The problem is not “untouched”. The current public status is closer to: resolved up to a finite check / resolved through existing work covering the relevant regimes. That is important, and I do not want to erase that work.

What seems to be missing, at least in the public form of the result, is a single end-to-end proof object: one auditable route that turns the whole conjecture into explicit local branches, finite certificates, checkable exits, and a global reassembly.

That is what this project is trying to provide.

To be clear: I’m not claiming peer review, not claiming a Lean/Coq formalization, and not asking anyone to trust an AI-generated proof.

But... this is a really solid proof-candidate / audit package.

The intended bridge is:

mathematical branch;
finite local certificate;
checker-accepted descent / classified exit / contraction;
global reassembly of the conjecture.

The repo includes:

a cleaned manuscript in paper/;
finite certificate checkers for the local blocks R, C0.3, H0-B+, U0simple, C0.1, and C0.2;
stored reports and reproducible certification scripts;
a small-prime computational backtest;
an external review guide listing the main weak points to attack.

Minimal reproduction:

git clone https://github.com/Atomicium-org/graham-rearrangement-certificates.git

cd graham-rearrangement-certificates

bash scripts/run_all.sh

Expected final line:

All default executable certification checks passed.

There is also a stronger stress run:

bash scripts/run_stress.sh

The arXiv preprint is ready and currently awaiting endorsement. I have reached out to several researchers active around this problem, and I’ll update the post with the arXiv link once it is live.

This was built during one very intense week with GPT-5.5 Pro assistance and a highly structured prompting workflow. The interesting question is not “did an AI solve it?” The interesting question is whether this kind of AI-assisted proof engineering can produce a certificate architecture that survives hostile mathematical audit.

The main places I would expect reviewers to attack are:

completeness of the visible description Vis;
legitimacy/minimality of the carrier support Car(T) in the R block;
contraction of perfect neutralities in C0.3;
coverage of H0-B+, U0simple, C0.1, and C0.2 by finite branch contracts;
the global reassembly from local exits back to the full conjecture.

If it fails, I want the first broken branch localized.

If it holds, it would be a complete certificate-style route for the full conjecture, not just a patchwork of asymptotic or externally distributed regimes.

Would love serious criticism from people interested in AI-assisted math, additive combinatorics, proof checking, or formalization workflows.