Each top-level directory is a self-contained Lake project with its own pinned toolchain, README, and build instructions.
The repository currently lists two projects. zeta23 formalizes a claim from Alpoge and Furman that more than two thirds of the zeros of the Riemann zeta function are simple and on the critical line. 3sum-apsp formalizes results from Alman and Vassilevska Williams, including word-RAM bounds of O(n^1.9992) for 3SUM and O(n^2.99942) for min-plus product and APSP on polynomial-size integers. The latter uses Lean 4 v4.33.1 and Mathlib v4.33.1.
The README says a project passes when lake build succeeds on its pinned toolchain with no sorry outside trusted comparator statement files, and when Palomar's acceptance check succeeds using the comparator, the nanoda kernel, and the landrun sandbox. The page does not provide a publication date or show the current check results for each project.