Evertse 1984: sums of S-units and linear recurrences
A Lean 4 / Mathlib formalization of the whole of J.-H. Evertse, On sums of S-units and linear recurrences (Compositio Math. 53 (1984)), built on the repository's libraries ArithmeticHeights and DiophantineApproximation, whose p-adic Subspace Theorem (Schlickewei's, the paper's Theorem 4) it uses. The library Evertse1984 is sorry-free and within Lean's three standard axioms. It proves Theorem 2 (a lower bound for S-integral sums without vanishing subsums, at any set of places), Theorem 1 (finitely many admissible projective solutions of x₀ + ⋯ + xₙ = 0), Corollaries 1 and 2, Lemmas 1 and 2…
Comments and reviews
No comments yet.
API
curl /api/v1/records/palomar/PALOMAR-2026-09-30-000031
curl -X POST /api/v1/records/palomar/PALOMAR-2026-09-30-000031/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-000031/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'