---

Claim. Let $d_1,\ldots,d_r\ge2$ be integers, repetition allowed, with $\sum_i1/(d_i-1)\ge1$. Then every nonnegative integer is $a_1+\cdots+a_r$, where each $a_i$ has only the digits $0$ and $1$ in base $d_i$, that is $a_i\in P(d_i,0)$ in the notation of Problem 124, with $a_i=0$ allowed. The Lean file linked above proves this as erdos_124, beside two versions of the formal-conjectures statement of the problem: for every k, every d : Fin k → ℕ with 2 ≤ d i for all i and 1 ≤ ∑ i, (1 : ℚ) / (d i - 1), and every n, there is a : Fin k → ℕ with the base-d i digits of each a i in {0, 1} and n = ∑ i, a i. The statement is stronger than the problem's first question, which asks only about sufficiently large integers and about distinct bases $d_i\ge3$. Boris Alexeev posted the result on the site's thread on 2025-11-29, writing that Aristotle from Harmonic found the proof working only from the formal statement. The file's header says the same and names no human author of the proof; the formal-conjectures statement file, at its commit of 2026-09-18 (the record link), marks its first question erdos124.zero as research solved, "solved by Boris Alexeev using Aristotle", with no formal_proof attribute. The argument was not reconstructed in this corpus.

Submission note. Posted to the site's forum by Boris Alexeev on 29 November 2025:

[Note: this comment was written before 2025/12/01, when the problem text was updated.]

Aristotle from Harmonic has solved this problem all by itself, working only from the formal statement! Type-check it online!

A formal statement of the conjecture was available in the Formal Conjectures project. Unfortunately, there is a typo in that statement, wherein the comment says $\geq 1$ in the display-style equation while the corresponding Lean says "= 1". (That makes the statement weaker.) Accordingly, I have also corrected that issue and included a proof of the corrected statement. Finally, I removed a lot of what I believed were unnecessary aspects of the statement, and Aristotle proved that too. In the end, there are three different versions proven, of which this is my favorite: theorem erdos_124 : ∀ k, ∀ d : Fin k → ℕ, (∀ i, 2 ≤ d i) → 1 ≤ ∑ i : Fin k, (1 : ℚ) / (d i - 1) → ∀ n, ∃ a : Fin k → ℕ, ∀ i, ((d i).digits (a i)).toFinset ⊆ {0, 1} ∧ n = ∑ i, a i I believe this is a faithful formalization of (a strengthening of) the conjecture stated on this page.

As mentioned by DesmondWeisenberg above, there's an issue involving the power 1 (which corresponds to the units digit here) that means the conjecture in [BEGL96] differs from this. I believe the version in [Er97] matches the statement here, in part because it lacks a gcd condition that is obviously necessary in [BEGL96]. I do not yet have access to [Er97e] to check the statement there. The subtlety of this issue is unfortunate, given Aristotle's achievement!

Timing-wise, Aristotle took 6 hours and Lean took 1 minute.

Covers. The first question, read as the problem page's corrected Statement, with $\sum_i1/(d_i-1)\ge1$: yes, and for every integer, not only the sufficiently large ones. Not covered: the second question, the one under the gcd condition with powers of exponent at least $k\ge1$, which the Lean file does not address.

Depends on. No page of this wiki.

Standing. Claimed. The claim was published by Boris Alexeev; the proof is Aristotle's, an AI system of Harmonic, named here as the thread post names it, so the Lean file is an independent proof and has its own page. The site's commentary (page last edited 1 December 2025) credits the proof of the first question to Aristotle through Alexeev, and the site's curator wrote on the thread on 2025-11-30 that the problem would stay open with the gcd condition added to the statement, which the rewrite of 1 December 2025 did; the site labels the problem OPEN, so the credit is commentary, not acceptance, and no reviewed evidence is listed. There is no written proof beyond the thread's sketch and no publication, so nothing is refereed. This corpus has not built or audited the Lean file, so the page lists no formalized evidence.