Monotone Local Search with Sample-Dependent Running Times: files for checking

lean/        the Lean 4 project (Mathlib). Check it with
               cd lean
               lake exe cache get
               lake build
               lake env lean CheckDecls.lean
             CheckDecls.lean checks that every declaration linked from the paper in the default
             target exists and prints its axioms. The RSC certificate data target (generated data
             modules, decided by native_decide) is separate: ancillary/README.md says how to build
             it, and CheckDeclsData.lean checks its linked declarations.

ancillary/   the computer certificates and their checkers (MIT licence). Check them with
               cd ancillary
               python3.12 -m venv .venv && .venv/bin/pip install -r requirements.txt
               PYTHON=.venv/bin/python ./verify_all.sh          (quick, about a minute)
               PYTHON=.venv/bin/python ./verify_all.sh --full   (full, one to two hours)
             The quick mode checks the checksums and every certificate that a proof depends on
             except the RSC antinorm certificate; only the full mode verifies that one, with two
             independent programs. Appendix F of the paper says what each program certifies.

Companion site: https://serggasp.github.io/sample-MLS-site/formalisation.html maps each
statement of the paper to its Lean declarations and certificates.
