FLMF: Verified Autoformalization of the Digital Library of Mathematical Functions

We present the Formalized Library of Mathematical Functions (FLMF), a Lean 4 counterpart to the NIST Digital Library of Mathematical Functions (DLMF). The DLMF records more than 8,000 identities for the special functions of mathematics and science across 36 chapters, together with the metadata that fixes each equation's conventions and scope. FLMF restates those identities as a typed, reusable Lean API of definitions and theorems, and proves them, so that downstream formalization in analysis and mathematical physics can cite special-function facts instead of rebuilding them. Because a library of this size cannot be written by hand, we build it with an agentic pipeline of three human-gated stages in which agents extract equations, write Lean statements, run checks, and construct proofs, while a human gates the output of every stage so that no stage can silently shrink its denominator. The pipeline's central difficulty is faithfulness: the Lean kernel certifies that a theorem follows from the definitions given to it, but not that the theorem is the claim named by its DLMF citation. We therefore make fidelity a separate acceptance gate, enforced by a validation protocol of three checks with distinct failure models. We have a back-translation check and a numerical check applied to the statement before any proof exists, and a vacuity check applied to the finished proof. We report chapter-level progress, describe misprints in the DLMF that the protocol uncovered, and propose the DLMF ground truth together with these checks as a benchmark and grading oracle for autoformalization.