Fetched erdosproblems.com/728 live (WebFetch was blocked with 403; curl with a browser user-agent succeeded). The page is marked PROVED (LEAN). Its literally displayed problem statement is one-sided (a+b > n + C log n, with no upper bound on a or b), and the page itself calls this ambiguous with known trivial solutions (AlphaProof-style very large a,b; also a=b=n). It explicitly endorses the Barreto/ChatGPT-5.2 log-sandwich construction (C1 log n < a+b-n < C2 log n) as answering the problem in the spirit intended. Separately fetched google-deepmind/formal-conjectures ErdosProblems/728.lean: its erdos_728 theorem (itself an unproved 'sorry' stub used only as a documented statement-of-record pointing at the external proof) states exactly this log-sandwich version. I then diffed that, term for term, against erdos_728_fc in the actual built upstream source (located via grep in my own checkout): identical quantifier/filter structure, identical variable names, identical conjunct order, identical docstring -- differing only by the cosmetic answer(True) wrapper formal-conjectures uses for its open/solved-problem bookkeeping. Also checked the natural-number-subtraction concern for (a+b-n)!: the hypothesis a+b > n + C*log n with C>0 and log n >= 0 for n>=1 structurally forces a+b>n before the subtraction is taken, so no truncation-based triviality is hiding there. Caveat: formal-conjectures' own local copy is unproved, so this is a statement-level textual match against the community-documented ground truth rather than a cross-check against an independently machine-verified equivalent formalization -- but a verbatim statement match is exactly what this claim asserts, and I confirmed that directly myself.

Independently reproduced the full kernel check from scratch (own clone, own temp directory, own machine, own execution) and confirm lake build ErdosProblems.Erdos728 succeeds (8580/8580 jobs, exact banner match), with both erdos_728 and erdos_728_fc sorry-free, depending only on [propext, Classical.choice, Quot.sound] per the raw compiler output I read myself rather than the wrapper script's summary. I also separately audited the faithfulness question flagged as the likely failure mode: erdosproblems.com/728 confirms the website's literal displayed statement is a known ambiguous/trivial one-sided inequality, while the theorem actually proved (erdos_728_fc) is a verbatim match, modulo a cosmetic wrapper, of the community-documented intended non-trivial log-sandwich statement in google-deepmind/formal-conjectures, which the site itself endorses as resolving the problem in spirit. All three claims hold up under adversarial scrutiny; I found no admitted gaps, no smuggled axioms or native_decide-style trust shortcuts, and no statement weakening.

Diffed the proved erdos_728_fc (Erdos728.lean:2013-2021) against google-deepmind/formal-conjectures ErdosProblems/728.lean (fetched raw): character-for-character identical modulo the `answer(True) ↔` wrapper — even the doc-comment is copied verbatim. It is the intended NON-trivial form: it imposes the two-sided window n+C·log n < a+b < n+C'·log n together with ε·n<a, ε·n<b. That upper bound rules out the trivial solutions (e.g. a=b=n) that satisfy the one-sided 'a+b > n+C·log n' question currently shown on erdosproblems.com. Positive/existence direction proved, matching the affirmative resolution.

I fetched the finding cold and independently re-ran the kernel check on a fresh clone of plby/lean-proofs@97957fb9 under leanprover/lean4:v4.32.0-rc1 + mathlib 360da6fa: `lake build` completed successfully (8580 jobs), and the build's own #print axioms output shows both erdos_728 and erdos_728_fc depend only on [propext, Classical.choice, Quot.sound] with no sorryAx anywhere — a genuine gap-free proof, verified by reading the axiom lines directly rather than trusting the script banner. The proved erdos_728_fc is byte-identical to the DeepMind formal-conjectures statement of #728 and encodes the intended non-trivial two-sided log-window version, not the trivial one-sided form displayed as the bare website question. All three claims hold up under adversarial checking; this is a faithful, sorry-free, independently reproduced formal verification of the positive resolution of Erdős #728.

Compared erdos_728_fc against formal-conjectures/728.lean reference. Statements identical except for answer(True) wrapper. Proved theorem correctly requires a+b in (n+C*log n, n+C'*log n), the non-trivial form.

All three claims verified independently. Build succeeds; axioms clean (no sorryAx); formalization faithfully captures intended non-trivial Erdos 728 form with logarithmic bound on a+b. Genuine positive resolution.