Comparator certificate

Shallow Learning Tends to Ridgelet Transform · 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 (LeanTends2Ridgelet.Setting.*). 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 the theorems of LeanTends2Ridgelet.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, instance arguments, hypothesis order, universe levels) from the library theorem; every section reproduces the open lines and the variable/include block of the source module so that both files elaborate to identical kernel terms, and both files set autoImplicit false.

Two statements are reformulated rather than copied verbatim: the library statements of bounds_of_isMinimizer and moments_of_isMinimizer mention a proof term of the theorem module Structure/GibbsMinimizer (memLp_condMeanAmp_of_isMinimizer, the fact MemLp (condMeanAmp ρ) 2 (hiddenMarginal ρ)); in thm_m1_bounds and thm_m1_moments this fact is an explicit hypothesis, which is definitionally the same statement by proof irrelevance.

Not included (only sorry-free library theorems are certified): thm:m1prime (c) (gradientFlow_convergence, Łojasiewicz argument), the Gaussian log-Sobolev inequality (Gross) used by lem:lsi/cor:uniform-lsi (satisfiesLSIParam_proximalGibbs) and hence cor:mfld-unconditional and thm:mfld-wellposed (thm:mfld-convergence is certified in its conditional form, with a uniform LSI as hypothesis), lem:minimizer (5), cor:joint-schedule-improved (i)(ii), auxiliary lemmas such as lem:operators (2)–(5), and the parts of the paper that are not formalized (Section 9, the homogeneous geometry and general spheres of Section 11, propagation of chaos).

Import closure of the challenge: the 17 modules LeanTends2Ridgelet.Setting.*, whose closure also contains Basic/Operators, ToMathlib/{Pinsker, SignedMeasureIntegral, HalfspaceVC}, ToFoML/{PseudoDimension, SauerShelahCovering}, ToOperatorRidgelet/SpectralPower and, from the dependencies, FoML.Defs, FoML.Entropy.Dudley and OperatorRidgelet.ToMathlib.* (general-purpose material needed by the definitions).

Mapping: paper label → challenge theorem → library declaration

How to reproduce

git clone https://github.com/shosonoda/lean-tends2ridgelet.git
cd lean-tends2ridgelet
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.