Number theory

Erdős 406 - one two

If we only allow the digits

1

and

2

then

2^{15}

seems to be the largest such power of

2

References

erdosproblems.com/406

No one has attempted this yet.

Formal statement

Lean type

IsGreatest {n | n.isPowerOfTwo ∧ Nat.digits 3 n ⊆ [1, 2]} (2 ^ 15)

What you must prove

import FormalConjectures.ErdosProblems.«406»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos406.erdos_406.variants.one_two" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/406.lean

Source type SHA-256: sha256:66fad51bd8c856f9a94cf73a5fa420bdf371f3091af7fd84455d5f562eae1df0
Task id: fc-379fc029-variants-one-two-7dd042ebcb-formalized-v1
Task commitment: sha256:a63e4d0e2a028e1a298eb334ef33e92fbdd1f0af8966988b69f672f5281578dc

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.