VibeMathed reports this item as resolved. VibeMath preserves that report as a source assertion and has not independently authored a plain-language mathematical explanation.
Precise statement
For coprime $b,c\ge 2$ the Stoneham constant $\alpha_{b,c}=\sum_{k\ge1}1/(c^{k}b^{c^{k}})$ is known to be $b$-normal. Bailey and Borwein asked in 2012 what happens to a sum of two of them sharing the base: with $b,c_1,c_2\ge2$, $(b,c_1)$ and $(b,c_2)$ coprime, is $\alpha_{b,c_1}+\alpha_{b,c_2}$ normal in base $b$? In their words, "it is not known at the present time whether the sum $\alpha_{b,c_1}+\alpha_{b,c_2}$ is $b$-normal".
The source statement is reproduced for indexing with attribution. Mathematical correctness requires domain-expert or mechanical review. VibeMath has not independently audited statement
fidelity, correctness, priority, or novelty.
What AI did
ChatGPT-6 Astra
The submitter states that the model chose the problem, proved it and produced the Lean formalisation. That is their account of their own project and is recorded at face value; as with this author's earlier xi-normality entry, the repository does not separate what a model did from what a person did, and the manuscript carries no author byline, so nothing found in review corroborates the autonomy claim beyond the submitter's word and nothing contradicts it.
Checked here on 12 September 2026 by reading the repository at commit f4d3d1f. Challenge.lean imports only Mathlib, writes the Stoneham series out in full, and states normality of the sum directly: for every length $l$ and every $j<b^{l}$, the proportion of overlapping starting positions $n<M$ whose shifted fractional part lands in the half-open radix cylinder tends to $b^{-l}$, under the coprimality hypotheses the paper asks for. Nothing project-defined appears in it. Solution.lean proves that exact proposition by unfolding definitions only, adding no analytic or normality assumption. Audit.lean pins the axiom lists of six declarations including the solution with #guard_msgs, so a changed list fails the build rather than printing a note, and GitHub Actions built from the pinned toolchain (Lean 4.34.0-rc2) and mathlib commit, ran that audit, and separately verified a sha256 fingerprint of the submitted statement - two green runs on 10 September. Unlike this author's xi-normality repository there is no comparator configuration, so there is no independent-kernel replay; the statement fingerprint covers statement tampering and Lean's own typechecking anchors the solution to the challenge. The build was not repeated here, and the correspondence to the 2012 paper was checked by reading Section 4 at source.
Yes: the sum of two Stoneham constants sharing a base is normal in that base, for every admissible pair of parameters, with overlapping occurrences counted. Not to be confused with what the same 2012 paper proves: its Theorem 3 shows a sum of two $B$-NONnormal Stoneham constants is $B$-nonnormal, which concerns a different base and the opposite property. The open half was normality in the common defining base $b$, and that is what this settles.
Known method families
argument (source-reported)
Source-reported tools: argument.
Independent: unknown · difference confidence: 0
What remains uncertain
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.
VibeMath has not independently verified the mathematical claim.
AI-attempt independence and training-data exposure are unknown unless explicitly documented.
VibeMath has not independently audited the mathematical statement, proof, or novelty claim.