RatpointsLean

ratpoints is a C program by Michael Stoll that finds the rational points of bounded height on the curves y² = F(x, z), where F is a binary form of even degree with integer coefficients, by sieving. This project builds a model of it in Lean 4 that mirrors the hardware-independent structure of the C code function by function, proves with Mathlib that the model meets a short specification for every choice of the sieving parameters, and links the model to the C code by a record of which Lean definition models which lines of C, checked in CI, and by differential tests.