Heights, Siegel's lemma, Roth's theorem and the Subspace Theorems in Lean
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,…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-25-000022
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-25-000022/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-25-000022/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'