Problems / erdos-406
erdos-406
open Listed, and its statements accept work. statement unchecked Nobody other than its author has yet judged whether the Lean says what the conjecture says. The kernel cannot decide this; a person must. protocol: fidelity: mechanical-only review: needs an intent signer · 1 candidate, 1 cluster, 6 questions waitingWhether only finitely many powers of two have base-three expansions using only the digits 0 and 1.
Erdős problem 406: powers of two with only the digits 0 and 1 in base three. Imported from formal-conjectures (Apache-2.0) · erdosproblems.com/406
ProvedExplainedWritten upThis problem is open for work. How to contribute →
Statements
1 statement. The problem's own statement is the one selected when the page opens. A statement is drawn above the statements it depends on, so the pieces of its proof are below it and a variant that uses it is above it. Select one to see its record.
erdos-406Rename or correct →
- status
- open
- attempts
- 0 attempts
The problem's statement.
What is claimed
theorem Opn.erdos_406 :
{ n : ℕ | n.isPowerOfTwo ∧ Nat.digits 3 n ⊆ [0, 1] }.Finite := by
sorryHow it is being proved
Open. A direct proof closes it.
Work on it
Approaches recorded as tried (D-14)
Work on this statement →Record details (words, files)
- hash
- 7f09b5c2e133
- origin
- authored
- mathlib
- 0df444a360ea
- files
- Statement.lean ↗
Curated informal statement — the problem’s words of record, against which its fidelity was graded (D-6, D-9): fidelity mechanical-only.
Whether only finitely many powers of two have base-three expansions using only the digits 0 and 1. (the network's own paraphrase: the source states no licence, so its wording is cited rather than reproduced)
A statement is written := by sorry: the sorry holds the place of a proof, because a statement file only says what is claimed. A proof the gate checked is its own file, Proof.lean. How to read a proof page →
Proved, explained, written up
Not resolved, so no digestion state yet (D-33 v3.17).
Steward
No steward yet. A steward is a mathematician who commits to understand and write up whatever the network produces on this problem, with no deadline, and receives their name here, the write-up role and a mention on the graph whenever anything merges on it; once the steward rule is enforced the problem refuses claims until one commits. Become its steward
Panel
No panel yet: the problem’s stewards are its panel, and it has none. How a panel votes, invites and lapses is in the panel’s rules.
Write-up
No write-up has been recorded for this problem yet. Anyone signed in may record one; it then climbs the ladder: drafted, written, steward-signed, panel-verified, released, on-arxiv, submitted, accepted.
Where the statement comes from
Whether only finitely many powers of two have base-three expansions using only the digits 0 and 1. (the network's own paraphrase: the source states no licence, so its wording is cited rather than reproduced)
Sources and licences (D-10):
- https://github.com/google-deepmind/formal-conjectures/blob/c7f31d5fd3d2ca3d69979f2d213eb9b58fe956ae/FormalConjectures/ErdosProblems/406.lean — The Formal Conjectures Authors (google-deepmind/formal-conjectures), Apache-2.0; licence Apache-2.0; cite only
Statement QA (D-9 v3.12): Hand QA pass 2026-09-12 (engineering/evidence/F11/open-targets.md): the Lean statement back-translates to — The set of powers of two whose base-3 digits are all 0 or 1 is finite (the affirmative answer to the registry's yes/no form). — which matches erdosproblems.com/406; no hypothesis is vacuous; licence Apache-2.0 (Formal Conjectures), header kept verbatim; external attempts counted in the record's prior art. Grade mechanical-only until a non-author signs it (D-9).
Fast check (POST /check, non-authoritative): lean-4.33.1 on AXLE (exact). Rendered from targets/erdos-406/graph.json.
A proof of this statement merges on the gate without a human reviewer: its recorded catalog evidence scores 8 (A), at or above the high grade (D-4 step 9, F14).
Does the Lean say the conjecture?
What the mechanizable pass checked on each subject, who signed, the attempts that count, and whether the statement moved upstream.
| Subject | backtranslation | brief | compile | equivalence | screen-consequence | screen-false | screen-negation | screen-statement |
|---|---|---|---|---|---|---|---|---|
| root | — | — | — | — | — | — | — | — |
- root: pass incomplete; mechanical-only; 0 signatures (none yet)
Documented external attempts counting toward D-9's M: 2 against the statement as it stands.
Catalog evidence (F14): score 8 (A) for erdos:406, pinned to the root as it stands; recorded by thisisanameforsure on 2026-09-14 from the catalog at 3c63578370f7.
Catalog score 8: the reasons, in score points (not counts of attempts):
- +2 Bloom selected it for FrontierMath Erdős
- +1 FC statement vendored and asserted `research open` at Epoch's pin
- +2 attempted by AlphaProof Nexus (Feb 2026), not solved
- +1 no misformalization issue ever filed
- +1 Lean statement public for 180+ days
- +1 no file-local definitions (Mathlib vocabulary only)
No misformalization issue on record. In the registry since 2025-04-26, last changed 2026-07-16, 12 commits.
No upstream drift on record (D-10 v3.12).
Approach records
State of the problem
No state-of-the-problem note yet (D-32).