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 intentionally curated (not “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, so this file stays a thin, stable import surface rather than duplicating long bibliographies.