Proof entry point used by downstream packages.
This module collects the maintained proof surface: tensor facts, autograd correctness, runtime-approximation theorems, model proofs, and verification soundness results.
Proof entrypoint #
Umbrella import for TorchLean's core proof infrastructure.
This is the set of proof modules that NN.Library considers part of the supported
library surface area (as opposed to tests, examples, or executable workflows).
Notes:
- This is curated rather than "import everything under
NN/Proofs". - If you add a new proof module that should be part of the stable surface, add it here.
Proof-facing landmarks:
- real-analysis and numerics-facing helper theorems:
NN.Proofs.Analysis, - analytic autograd correctness:
NN.Proofs.Autograd.FDeriv.*, - tape/DAG reverse-mode correctness:
NN.Proofs.Autograd.Tape.*, - model-level invariants:
NN.Proofs.Models, - probability-kernel facts:
NN.Proofs.Probability, - runtime-approximation bounds:
NN.Proofs.RuntimeApprox.*, - verification envelopes and backend bridges:
NN.Proofs.Verification.
References / context:
- PyTorch autograd background: https://pytorch.org/docs/stable/autograd.html
- The theorem bundles re-exported here document the math/model references they rely on locally.