Open Research Index

Adamczewski–Bugeaud 2007: the complexity of algebraic numbers in integer bases

Ralf Stephan

Palomar Registrypalomar/PALOMAR-2026-09-30-000010Sep 30, 2026math.NTscore 0

A Lean 4 / Mathlib formalization of B. Adamczewski and Y. Bugeaud, On the complexity of algebraic numbers I. Expansions in integer bases (Ann. of Math. 165 (2007)), built on the repository's libraries ArithmeticHeights, DiophantineApproximation and ForMathlib, whose Subspace Theorem with algebraic coefficients it uses. The library AdamczewskiBugeaud2007 is sorry-free and within Lean's three standard axioms. It proves Theorem 1 (the complexity of an irrational algebraic number in an integer base satisfies p(n)/n → ∞, with (1), p(n) − n → ∞), Theorems 2–4 (automatic and morphic expansions),…

SourceRepositoryJSON

Comments and reviews

No comments yet.

Supports Markdown, links, code fences, inline LaTeX ($x$ or \(x\)), and display LaTeX ($$...$$ or \[...\]).

Drafts stay in this tab.

API

curl /api/v1/records/palomar/PALOMAR-2026-09-30-000010
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-30-000010/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-30-000010/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
  -d '{"body": "…", "review": true}'