Binary normality of a localized logarithm value

Let $\xi=\sum_{a,c\ge 0}\frac{1}{2^{a}3^{c}\,2^{2^{a}3^{c}}}$ , the value at $1/2$ of Dibag's logarithm localized at the primes $2$ and $3$ ; summing the same terms over every positive integer rather than only the $3$ -smooth ones gives $\log 2$ . Is $\xi$ normal in base two, that is, does every finite binary word of length $l$ occur in its binary expansion with limiting frequency $2^{-l}$ , counting overlapping occurrences?

Result: Proved(see note)
Status: Resolved
AI contribution: AI-discovered
Method: Argument
Field: Normal numbers and digit expansions
Posed by: —
Year posed: —
Years open: —
Solved: 2026-09-09
Model: ChatGPT-6 Astra
Vendor: OpenAI
Collaborators: —
Verification: Lean-verified
Publication: Preprint
Significance: 15 / 100
Disclosed cost: —
Wikipedia: No dedicated article

What was actually shown

Yes. Every finite binary word occurs with its expected limiting frequency, overlapping occurrences counted. The one-prime members of this family were already known to be normal: $\alpha_{b,p}=\sum_{k\ge1}p^{-k}b^{-p^{k}}$ is Stoneham's constant, proved normal under primitive-root hypotheses by Stoneham in 1973 and unconditionally for coprime parameters by Bailey and Crandall in 2002. The new content is the mixed-prime support, where all the indices $2^{a}3^{c}$ contribute at once and the argument turns on the largest power of three in the truncation denominator surviving addition. The paper states that it has not located an earlier published conjecture about $\xi$ , so this settles no previously posed question. The Lean development covers qualitative normality of this constant only; the paper's quantitative discrepancy bound and its extension to larger finite sets of primes are outside the formalisation.

What the AI did

The submitter states that ChatGPT-6 Astra chose the problem, proved it and produced the Lean formalisation. The repository's own credits are less specific: they describe an AI-assisted mathematical project, attribute the submission documentation and interface to OpenAI Codex, and do not separate what a model did from what a person did. The paper carries no author byline. Nothing found in review corroborates the autonomy claim beyond the submitter's word, and nothing contradicts it; it is recorded as their account rather than as an established fact.

Verification

Checked here on 10 September 2026 by reading the repository at commit 0696181. Challenge.lean imports only Mathlib.Analysis.Real.OfDigits, writes the constant out in full as the double sum, and states normality directly: for every length $l$ and every $j<2^{l}$ , the proportion of starting positions $n<M$ whose shifted fractional part lands in $[j/2^{l},(j+1)/2^{l})$ tends to $2^{-l}$ . No project-defined normality predicate and no project-defined constant appears in it, which is where a faithful-looking statement could have been quietly weakened, and the statement takes no extra hypotheses that could carry an unproven input. Solution.lean derives that statement from the development, and comparator.json compares XiComparator.normality with only propext, Classical.choice and Quot.sound permitted. Audit.lean pins the axiom lists with #guard_msgs, so a changed list fails the build rather than printing a note. GitHub Actions built the project twice on 9 September from the pinned toolchain (Lean 4.34.0-rc2) and the pinned mathlib commit and passed, which puts the kernel check on a machine other than the author's. The build was not repeated here, and the repository's README records that no external statement audit has been made.

Sources

Submitted by nufrogcaca on 09 Sep 2026

Binary normality of a localized logarithm value

What was actually shown

What the AI did

Verification

Sources

Discussion