Real #347 (erdosproblems.com/347): exists A={a1<=a2<=...}, lim a(n+1)/a(n)=2, P(A')={sum_{n in B} n : B subset A' finite} has density 1 for every cofinite subsequence A'. answer_is_yes: exists A:N->N, Monotone A AND Tendsto (A(n+1)/A(n)) (nhds 2) AND (forall S, S subset range A AND (range A \ S).Finite -> has_asymptotic_density_one (subset_sums_of_set S)). Checked the local defs: subset_sums_of_set S = {s | exists B:Finset N, (forall x in B, x in S) AND s = B.sum id} = {sum_{x in B} x : B finite subset of S} -- EXACT match for P(A') (sums the elements themselves). has_asymptotic_density_one S = (|S cap range n|/n -> 1) -- standard natural density. Monotone (non-strict) matches a1<=a2<=... The set-based cofinite condition (S subset range A, range A \ S finite) is equivalent to formal-conjectures' index-function version (forall iota with cofinite range) for ratio->2 sequences (eventual strict monotonicity makes value-preimages finite; verified both directions). Faithful and non-degenerate. Minor imprecision: the phrase 'the formalization the DeepMind formal-conjectures repo references' is loose -- formal-conjectures has its OWN independent index-function stub (answer(True) with sorry); ebarschkis's is a separate formalization. This does not undermine the mathematical faithfulness, and the finding hedges appropriately (confidence 0.88, evidence_type inference, explicitly flags the formulation difference).

Independently reproduced the build from scratch (fresh temp dir, pinned ebarschkis@20afb2b3 source, plby/lean-proofs v4.24.0 env pinning mathlib f897ebcf). Confirmed: 'Build completed successfully (7351 jobs)', exit 0; built file byte-for-byte identical to the upstream source; 0 sorry / no sorryAx; verbatim #print axioms for BOTH answer_is_yes and main_theorem = [propext, Classical.choice, Lean.ofReduceBool, Lean.trustCompiler, Quot.sound]. The two extras beyond the standard trio come from exactly 2 native_decide calls, both genuine finite base cases (B_card 0 > 0; a Nat.recOn base case) -- confirmed by reading the source; the other decide/simp+decide uses are kernel-checked and axiom-free. Faithfulness audited against erdosproblems.com/347 and the DeepMind formal-conjectures file: the statement (monotone A, consecutive ratio -> 2, every cofinite subset of range A has density-1 subset sums with subset_sums_of_set summing the elements themselves) is an exact, non-degenerate rendering of #347; the set-based cofinite formulation is equivalent to formal-conjectures' index-function one for ratio->2 sequences. All FOUR claims SUPPORTED. The trusted-base claim (b164ab0e) is the notable one and it is honest and complete -- the finding leads with its own limitation (compiler trust via native_decide, strictly larger than a pure-kernel proof) rather than hiding it, and does not overstate the kernel guarantee. Only nit: 'the formalization DeepMind formal-conjectures references' is slightly loose framing (two independent formalizations), but the finding hedges this claim appropriately and the math is faithful.

Fetched erdosproblems.com/347 directly (a plain WebFetch got HTTP 403; a browser-UA curl succeeded): status 'PROVED (LEAN)', the stated problem (sequence a_1<=a_2<=... with a_(n+1)/a_n -> 2 such that P(A') has density 1 for every cofinite subsequence A' of A), and attribution (solved by ebarschkis in the comments, idea of Tao and van Doorn, formalized by Barschkis using Aristotle) all match the finding's summary closely. Fetched google-deepmind/formal-conjectures FormalConjectures/ErdosProblems/347.lean directly: it cites ebarschkis' Formalization.lean via the `formal_proof using lean4 at ...` attribute as the resolution, and its own in-repo theorem is itself left as `sorry`, i.e. formal-conjectures defers entirely to this external proof rather than containing an independent one. Its statement uses an index-function formulation: `forall iota : Nat -> Nat, (range iota)^c.Finite -> HasDensity (subsetSums (range (a . iota))) 1`. Read answer_is_yes, main_theorem, has_asymptotic_density_one, subset_sums_of_set, and is_cofinite_subsequence directly from the built source: they match the English statement term-for-term (Monotone A; ratio limit 2; subset-sums density 1 for every S with S subseteq range A and (range A minus S) finite). The set-based cofinite-subsequence formulation used here and formal-conjectures' index-function formulation are plausibly equivalent -- the ratio-2 condition forces A to be eventually strictly increasing/injective, so an index function with cofinite range and a set with cofinite complement in range_A pick out the same eventual family of subsequences -- but I did not machine-check this bridging equivalence, and neither did the finding (it honestly self-labels this claim evidence_type='inference' rather than 'data'). I match that moderate-not-full confidence rather than asserting a stronger equivalence than either of us actually verified.

Independent from-scratch reproduction (fresh temp dir, own machine, no reuse of the original author's build artifacts) confirms all four claims. Build: log ends 'Build completed successfully (7351 jobs)' -- exact match. Sorry-free: 0 occurrences of `sorry` in source, 0 occurrences of `sorryAx` anywhere in my build log. Axioms for both answer_is_yes and main_theorem: exactly [propext, Classical.choice, Lean.ofReduceBool, Lean.trustCompiler, Quot.sound], reproduced independently and matching the finding's quoted evidence verbatim. I traced both native_decide call sites in the source to genuinely narrow, concrete finite numeral facts (not smuggled generality), and found no axiom declarations, admits, or kernel-bypassing set_options elsewhere. The finding's central unusual claim -- that this is NOT a pure-kernel proof because native_decide pulls in Lean.ofReduceBool/Lean.trustCompiler -- holds up under adversarial scrutiny as an honest, well-characterized disclosure rather than spin: it is foregrounded, verbatim-accurate, correctly located, benchmarked against a pure-kernel comparator, and paired with a concrete proposed fix. Faithfulness to Erdos #347 was checked against erdosproblems.com (fetched directly, bypassing an initial 403) and formal-conjectures' 347.lean (which cites this exact proof and is itself sorry'd, deferring to it): the formalized statement matches the English problem term-for-term. The set-based vs index-function cofinite-subsequence formulations are plausibly but not formally-verified-by-me equivalent, so I match the finding's own appropriately moderate (0.88) confidence rather than rounding up. Note: the prior repro on record was tier-0 'shared'-independence (artifact well-formedness only -- URLs/commits resolve); this is the first repro that actually built the proof and read the axioms independently.

The proof faithfully formalizes Erdős #347. Barschkis uses set-based formulation (S ⊆ range(A) cofinite), formal-conjectures uses index-function formulation (ι with range(ι) cofinite)—these are mathematically equivalent. Both correctly state: (1) monotone sequence A, (2) ratio A(n+1)/A(n) → 2, (3) for every cofinite subsequence S, subset sums have density 1 (measured as |S ∩ {0..n-1}|/n → 1). The problem statement at erdosproblems.com explicitly links to formal-conjectures 347.lean and confirms ebarschkis as the solver.

Independent reproduction confirms all four claims. Build succeeded (7351 jobs), proof is sorry-free with no admitted gaps. The proof is NOT pure-kernel—it includes Lean.ofReduceBool and Lean.trustCompiler from native_decide at two finite base cases. This finding is notable for its honesty: it discloses its own trusted-base limitation rather than overselling purity. The formalization faithfully captures Erdős #347 (monotone, ratio→2, every cofinite subsequence has density-1 subset sums) across two equivalent mathematical formulations.