Comparator certificate

Generalization error bounds for deep models · Sho Sonoda

← Project page · Blueprint · comparator/ on GitHub

Latest verification result

Last three lines of the output of ./script/comparator.sh:

Running Lean default kernel on solution.
Lean default kernel accepts the solution
Your solution is okay!

What Comparator certifies

Comparator takes a challenge (theorem statements with the proofs replaced by sorry) and a solution (the same statements with proofs), exports both environments with lean4export and checks, for every theorem listed in the configuration, that:

• Statement equality. The theorem's type in the solution is identical to its type in the challenge, and every constant occurring in the statement is identical in both environments (definitions cannot be silently changed to make the theorem easier).
• Permitted axioms. The proof depends on no axiom outside the permitted list (propext, Quot.sound, Classical.choice); in particular no sorryAx and no project-specific axiom.
• Kernel replay. Lean's default kernel re-checks the exported solution independently of the elaborator, so the certificate does not rely on tactics or on lake build alone.

Everything in the import closure of the challenge is the trusted vocabulary of the certificate. comparator/Challenge.lean imports only the definition modules of the library (LeanDeepgen.Setting.*, Profiles.Defs, Tradeoff.Defs, Growth.Defs) and the example modules holding the definitions of the worked examples; the general-purpose tools come from lean-rademacher (FoML.ToMathlib, FoML.ToFoML). The statements are the paper's theorems in their Lean form, that is, with the corrections and generalizations described in the README.

Configuration

comparator/config.json lists 64 theorems of LeanDeepgen.Challenge (challenge module Challenge, solution module Solution; both are Lake libraries with srcDir = "comparator") and the three permitted axioms. Each challenge statement is copied verbatim (binders, implicitness, hypothesis order, universe levels) from the library theorem; the open lines of each section reproduce the context of the source module so that both files elaborate to identical kernel terms. The one exception is thm_dudley_subgaussian, whose auxiliary definitions live in a theorem module and are therefore unfolded inline in the challenge.

Not included: the cited theorems thm:guivarch-bass, cor:nilpotent-entropy, thm:breuillard-large-balls (not formalized; P2 takes their conclusion as a hypothesis), the Φ∞ part of lem:cot-output, and the integral identity of lem:log-split (used inside the proofs of prop:profiles (ii)/(iv)).

Note (2026-09-26): thm:rad.decomp.ent.ent (both forms) and thm:caa are a different case — they are formalized and remain in the challenge, but the manuscript was pruned on 2026-09-26 and no longer prints the corresponding appendix sections (formerly App. E, “A deterministic entropy alternative to thm:hidden-decomp”, and App. P, “Compact-Domain Arzelà–Ascoli Principle for Self-Maps”, in the pre-2026-09-26 lettering — not to be confused with the current Appendix E, “The Sudakov-type converse”, a different section under the reorganized lettering A–M introduced later the same day). The Lean modules Bounds/EntropyDecomp, Bounds/EntropyDecompSample and Growth/ArzelaAscoli are unchanged.

Note (2026-09-26, appendix reorganization): the manuscript's appendix was further reorganized the same day into a fixed order and lettering A–M (see SUMMARY.md): A conventions/basic facts, B literature, C bias–variance, D hidden–output, E the Sudakov-type converse (thm:sudakov-type, cor:matching, cor:sudakov-rates, prop:global_scalar_observable, prop:linear-interpolation, cor:rkhs-readout), F growth mechanisms, G the layerwise envelope, H variance profiles, I the four regimes and balancing depths, J teacher–student/neural-operator/implementation examples (prop:implementation, proof now in J.3), K deep ReLU networks, L chain-of-thought symbolic computation, M unrolled iterative solvers and samplers. All Lean labels referenced in the table below are unchanged by this reorganization; only their location within the appendix moved.

Mapping: paper label → challenge theorem → library declaration

How to reproduce

git clone https://github.com/shosonoda/lean-deepgen.git
cd lean-deepgen
lake exe cache get && lake build

# once: Comparator and lean4export (for this project's Lean version) in ../comparator-tools/
mkdir -p ../comparator-tools && cd ../comparator-tools
git clone https://github.com/leanprover/comparator.git && (cd comparator && lake build comparator)
git clone --branch v4.32.0 https://github.com/leanprover/lean4export.git lean4export-v4.32.0 && (cd lean4export-v4.32.0 && lake build)
cd -

./script/comparator.sh   # about a minute; ends with "Your solution is okay!"

The script builds Challenge and Solution, exports them and runs the checker on comparator/config.json. On Linux it uses landrun for sandboxing when available and Comparator's fake-landrun shim otherwise (always on macOS). The tool locations can be overridden with COMPARATOR_TOOLS, COMPARATOR_BIN, COMPARATOR_LEAN4EXPORT and COMPARATOR_LANDRUN.