Verified Deep Learning with Lean 4

A Axioms at a glance

The Verified VJP Proofs suite contains 30 axioms and 48 theorems across nine Lean files, with zero sorrys. The axioms fall into three buckets:

  • Calculus primitives (8): chain rule, linearity, product rule, identity, reindex — elementary facts about the partial-derivative function \(\operatorname {pdiv}\). Correspond directly to Mathlib HasDerivAt / HasFDerivAt lemmas.

  • Elementary Jacobian facts (about 11): the Jacobian of a specific operation (ReLU diagonal, softmax rank-1, layer-norm 3-term, etc.), stated in \(\operatorname {pdiv}\)-land rather than bridging to Mathlib.

  • Bundled layer VJPs (about 11): each opaque forward (conv2d, depthwiseConv2d, mhsa_layer) paired with a bundled \(\mathsf{HasVJP}\) existence claim. Gradient-checked numerically in check_axioms.py.

Everything else — 48 theorems — is composition over these axioms, glued by the three structural rules (chain, fan-in, product) and five closed-form Jacobian tricks (diagonal, sparse toeplitz, binary selection, rank-1 correction, outer product).