Problem10_32.lean`

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL: Lean4 Domain Explanation Language

Annotation provenance. This overlay contains 10 curated AI-written annotations and 7190 mechanical source-derived annotations. They have not been human-reviewed as explanations; treat them as unverified and not mathematical authority. Retained generation history: The 71 original curated annotations were produced in a Claude Sonnet 5.5 session at medium effort; Claude Opus 5.5 is recorded in that session as the advisor model, not the direct author. The bulk source-derived expansion was generated mechanically from pinned source comments by tooling developed in a GPT-5.6 Sol session at ultra reasoning; GPT-5.6 Sol did not originate the quoted source prose. On 2026-10-17 the mechanically generated source-comment annotations of the Formal Conjectures, Carleson, FLT, PFR, CompFiles, Mathematics in Lean and Theorem Proving in Lean overlays were regenerated by the same generator after three corrections made in a Claude Sonnet 5.5 session: titles no longer cut a sentence inside mathematics or end on a dangling word, workflow markers are removed from the quoted prose, and declaration names follow the scanner's namespace resolution. The boilerplate step line was dropped, and comments that were only a row of dashes no longer yield annotations. No new prose was written and no human review is claimed.

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

3 declarations, 1 contain sorry, 0 declared as axioms

Bugeaud Collection of Conjectures and Open Questions: Automatic Expansions in Two Bases

Problem 10.32 asks whether some irrational real number has automatic expansions in two multiplicatively independent bases. The answer is no. Adamczewski and Faverjon [AF20] proved it with the multivariate Mahler method, in a form that is stronger than the question asked: the base-$b$ digit sequence may be $k$-automatic for an arbitrary $k \ge 2$, not only for $k = b$.

The definitions used here are in FormalConjecturesForMathlib: Nat.MultiplicativelyIndependent and Nat.MultiplicativelyIndependentFamily, AutomaticSequence.IsAutomatic, AutomaticSequence.IsAutomaticInBase and AutomaticSequence.IsBroadlyAutomaticInBase.

References:

AF20 Adamczewski, Boris, and Colin Faverjon. "Mahler's method in several variables and finite automata." arXiv:2012.08283 (2020). Appendix A, Conjectures A.2 and A.3, both proved there from Part (i) of Theorem 1.1.
[AS03] Allouche, Jean-Paul, and Jeffrey Shallit. "Automatic Sequences: Theory, Applications, Generalizations." Cambridge University Press, 2003. Chapter 13, Open Problems 7, p. 403, is the problem that Problem 10.32 modifies.
[Bug12] Bugeaud, Yann. "Distribution modulo one and Diophantine approximation." Vol. 193. Cambridge University Press, 2012. Chapter 10.
[Cob69] Cobham, Alan. "On the base-dependence of sets of numbers recognizable by finite automata." Mathematical Systems Theory 3 (1969): 186-192.
[LvdP82] Loxton, John H., and Alfred J. van der Poorten. "Arithmetic properties of the solutions of a class of functional equations." Journal für die reine und angewandte Mathematik 330 (1982): 159-172. Its transcendence method was the first attack on the problem; Nishioka later reported a gap in its main proof.

Imports (1)

FormalConjecturesUtil

theorem Bugeaud32.adamczewski_faverjon Adamczewski–Faverjon [AF20, Conjecture A.3], proved there from Part (i) of Theorem 1.1 sorry line 71 source
Source documentation
Adamczewski–Faverjon [AF20, Conjecture A.3], proved there from Part (i) of Theorem 1.1. Let $b_1, \dots, b_r$ be multiplicatively independent positive integers, and for every $i$ let $\xi_i$ be a real number that is automatic in base $b_i$. Then $\xi_1, \dots, \xi_r$ are algebraically independent over $\mathbb{Q}$, unless one of them is rational.
Two points of fidelity. The hypothesis is the joint multiplicative independence of $b_1, \dots, b_r$ that [AF20] defines on p. 3 (no nonzero integer tuple $(n_i)$ has $\prod_i b_i^{n_i} = 1$), not the weaker pairwise condition; it is what the proof feeds to Part (i) of Theorem 1.1, via the multiplicative independence of $1/b_1, \dots, 1/b_r$. Automaticity is the broad notion that the proof of Conjecture A.3 uses: the base-$b_i$ digits of $\xi_i$ are $k$-automatic for some $k \ge 2$, which need not be $b_i$.

depends on sorry what this means
Statement uses: Nat, Fin, LE.le, OfNat.ofNat, Nat.MultiplicativelyIndependentFamily, Real, AutomaticSequence.IsBroadlyAutomaticInBase, Irrational, AlgebraicIndependent, Rat
Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous
28 instances, coercions and auxiliary constants left out.

Tactic trace: 1 steps
Open to load the checked before-and-after goal states.
```
theorem adamczewski_faverjon {r : ℕ} (b : Fin r → ℕ) (hb : ∀ i, 2 ≤ b i)
    (hind : Nat.MultiplicativelyIndependentFamily b)
    (ξ : Fin r → ℝ) (hauto : ∀ i, IsBroadlyAutomaticInBase (b i) (ξ i))
    (hirr : ∀ i, Irrational (ξ i)) :
    AlgebraicIndependent ℚ ξ := by
…
```
Mentions: Nat.MultiplicativelyIndependentFamily
theorem Bugeaud32.problem_10_32.variants.strong Problem 10.32, strong form line 85 source
Source documentation
Problem 10.32, strong form. No irrational real number is automatic in two multiplicatively independent bases, in the broad sense that its digit sequence in each of the two bases is k-automatic for some k. This is [AF20, Conjecture A.2], with the broad notion of automaticity that its proof provides.

depends on sorry what this means
Statement uses: Real, Irrational, Nat, LE.le, OfNat.ofNat, Nat.MultiplicativelyIndependent, AutomaticSequence.IsBroadlyAutomaticInBase, False
Proof uses: AlgebraicIndependent, Fin, Nat.succ, Rat, Matrix.vecCons, Matrix.vecEmpty, Bugeaud32.adamczewski_faverjon, List, List.Mem, Eq, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt and 24 more
27 instances, coercions and auxiliary constants left out.

Tactic trace: 14 steps
Open to load the checked before-and-after goal states.
```
theorem problem_10_32.variants.strong (ξ : ℝ) (hξ : Irrational ξ) (b₁ b₂ : ℕ)
    (hb₁ : 2 ≤ b₁) (hb₂ : 2 ≤ b₂) (hind : Nat.MultiplicativelyIndependent b₁ b₂)
    (h₁ : IsBroadlyAutomaticInBase b₁ ξ) (h₂ : IsBroadlyAutomaticInBase b₂ ξ) : False := by
…
```
Mentions: Nat.MultiplicativelyIndependent
theorem Bugeaud32.problem_10_32 Problem 10.32 line 103 source
Source documentation
Problem 10.32. Is there an irrational real number whose expansions in two multiplicatively independent bases can both be generated by a finite automaton? The answer is no, by [AF20].

depends on sorry what this means
Statement uses: Iff, False, Exists, Real, And, Irrational, Nat, LE.le, OfNat.ofNat, Nat.MultiplicativelyIndependent, AutomaticSequence.IsAutomaticInBase
Proof uses: iff_of_false, not_false, Bugeaud32.problem_10_32.variants.strong, AutomaticSequence.IsAutomaticInBase.broad
6 instances, coercions and auxiliary constants left out.

Tactic trace: 3 steps
Open to load the checked before-and-after goal states.
```
theorem problem_10_32 : answer(False) ↔
    ∃ ξ : ℝ, Irrational ξ ∧ ∃ b₁ b₂ : ℕ, 2 ≤ b₁ ∧ 2 ≤ b₂ ∧
      Nat.MultiplicativelyIndependent b₁ b₂ ∧
      IsAutomaticInBase b₁ ξ ∧ IsAutomaticInBase b₂ ξ := by
…
```
Mentions: Nat.MultiplicativelyIndependent