phillipkerger/zero-order-bounds-lean-verification

This repository holds a formal, machine checked proof written in the Lean proof assistant, built to accompany a mathematics research paper about optimization algorithms. It is aimed at researchers in mathematics and computer science rather than general software developers, and its purpose is to verify, line by line, that a specific mathematical claim in the paper is actually true. The claim itself is about a type of optimization problem called derivative free convex optimization, where an algorithm can only ask for the exact value of a function at chosen points, never its slope or direction. The paper argues there is a hard limit on how accurately any such algorithm can find the lowest point of the function within a fixed number of questions, and this repository proves that limit is real using Lean, a tool that checks every logical step of a proof so nothing can be waved through by hand. The repository contains two separate, independently checkable results. The first and simpler one is an older bound already proven and kept unchanged. The second is a sharper, more complete result from the same paper, fully verified here, including the more advanced geometric arguments the paper relies on, such as spherical averaging and a classical inequality called Brunn-Minkowski. The authors are careful to note that only the paper's lower bound claim is verified this way. Other parts of the paper, such as upper bound results, are explicitly outside what this repository checks. To build and verify the proofs yourself, you install a Lean tool called Elan, then run a series of build commands that compile each proof file and check it against a trusted, zero shortcut verification mode, meaning the proof is confirmed from first principles rather than relying on cached results. The repository also includes comparison tooling to check the proof's statements and assumptions against the paper's text. No license information is given in the README.