6. Verification and Certificates🔗

This chapter explains what TorchLean means by verification. The core pattern is always the same: name the semantic object, run or import a concrete artifact, check the artifact against the semantic object, and state which theorem or trust boundary connects the check to the intended ML claim.

The chapter covers the main verification families in the repository: IBP/CROWN and LiRPA-style bound propagation, autograd soundness, runtime approximation, compiler correctness, learning and optimization theory, scientific ML certificates, and external artifacts produced by Python, Julia, or verifier tools such as α,β-CROWN. The important distinction is not "inside Lean good, outside Lean bad." External tools are useful. TorchLean's job is to make the handoff explicit: what did the tool produce, what did Lean parse or recompute, and what remains a named assumption?

1. 6.1. Verification
2. 6.2. Proof Systems Beyond Bounds
3. 6.3. Autograd Proofs
4. 6.4. Runtime Approximation
5. 6.5. Learning Theory
6. 6.6. Optimization Theory
7. 6.7. Self Supervised Theory
8. 6.8. Approximation Theory
9. 6.9. Classical ML Proofs
10. 6.10. Probability and Gradient Utilities
11. 6.11. Scientific ML Verification
12. 6.12. Verification Certificates
13. 6.13. Two-Stage Verification Workflows