{"id":"palomar/PALOMAR-2026-09-27-000002","url":"https://github.com/rwst/Subspace-Theorems/tree/d7a11cb1dcab3883fd1008db27a8382c95455b0a","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-27-000002-v1.json","repo":"https://github.com/rwst/Subspace-Theorems","tags":["math.NT","msc:11J68","msc:11R06","msc:11J70","msc:11A55","msc:11J87","diophantine-approximation","lean-formalization","mahler-problem","algebraic-numbers"],"score":0,"title":"Corvaja–Zannier 2004: rational approximations to the powers of an algebraic number","trust":"high","domain":"math.NT","source":"palomar","authors":["Ralf Stephan"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 / Mathlib formalization of the whole of P. Corvaja and U. Zannier, On the rational approximations to the powers of an algebraic number: solution of two problems of Mahler and Mendès France (Acta Math. 193 (2004)), built on the repository's libraries ArithmeticHeights and DiophantineApproximation, whose Subspace Theorem it uses. The library CorvajaZannier2004 is sorry-free and within Lean's three standard axioms. It proves the Main Theorem (finitely many non-pseudo-Pisot δqu that are very close to integers, u in a finitely generated group of algebraic numbers), Theorem 1 (Mahler's…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-27","reactions":{},"formalized":true,"formalizes":[{"title":"On the rational approximations to the powers of an algebraic number: solution of two problems of Mahler and Mendès France","identifier":"","relationship":"formalizes"}]}