{"id":"palomar/PALOMAR-2026-09-25-000022","url":"https://github.com/rwst/Subspace-Theorems/tree/d12aa25a9725e8d28c1bfc018c664b7ceb8d35c5","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-25-000022-v1.json","repo":"https://github.com/rwst/Subspace-Theorems","tags":["math.NT","msc:11J87","msc:11J68","msc:11G50","msc:11J25","msc:11H06","msc:11D61","msc:11D57","msc:11D59","diophantine-approximation"],"score":0,"title":"Heights, Siegel's lemma, Roth's theorem and the Subspace Theorems in Lean","trust":"high","domain":"math.NT","source":"palomar","authors":["Ralf Stephan"],"reviews":0,"subject":"math.NT","summary":"A Lean 4 / Mathlib development of Schmidt's Subspace Theorem and the theory beneath it, following Bombieri–Gubler, Heights in Diophantine Geometry (Chapters 1–7), and Schmidt's route in general. Two libraries, sorry-free and within Lean's three standard axioms. ArithmeticHeights builds heights of points, polynomials, matrices and linear subspaces, Northcott and Kronecker, Minkowski's second theorem, Siegel's lemma and the Bombieri–Vaaler theorems. DiophantineApproximation builds on it Roth's theorem over a number field with several places (and Ridout, the p-adic form, targets at infinity,…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-25","reactions":{},"formalized":true,"formalizes":[{"title":"Heights in Diophantine Geometry","identifier":"","relationship":"formalizes"},{"title":"Diophantine Approximation","identifier":"","relationship":"adapts"},{"title":"On Siegel's lemma","identifier":"","relationship":"formalizes"},{"title":"On the Quantitative Subspace Theorem","identifier":"","relationship":"formalizes"}]}