Lean4-MLIR

Lean 4 → MLIR → GPU

Interactive proof blueprint: brettkoonce.github.io/lean4-mlir/blueprint/ (or PDF) — clickable dependency DAG for the full VJP proof suite (no sorrys, zero project axioms), from pdiv primitives up to the whole-network VJPs (ViT, ResNet, MobileNetV2, ConvNeXt, EfficientNet).

Lean 4 as a specification language for neural networks. Declare architecture in Lean, generate StableHLO MLIR (forward + loss + backward + optimizer all in one fused function), compile to GPU via IREE, train end-to-end. No Python runtime, no autograd library — the gradients are computed at codegen time in Lean.

Companion code for the upcoming book Verified Deep Learning with Lean 4 (follow-up to Convolutional Neural Networks with Swift for TensorFlow, Apress).

Current version: v0.6.0 — Object detection joins the framework. A YOLOv1 person detector on Pascal VOC, bootstrapped from Chapter 6's ResNet-34 backbone with a 1×1 convolutional detection head — the FC head can't learn localization on a small dataset (diagnosed end to end in planning/yolo_v5.md); the focal-loss objectness term is the remaining piece, flagged in the bestiary's new detection intro. The IREE/Lean training path gains global-norm gradient clipping, env-var checkpoint resume (LEAN_MLIR_INIT_LOAD / LEAN_MLIR_START_STEP), and per-step LR warmup. Blueprint adds demo-anchored intros for object detection (§11.2.2) and diffusion (§11.2.7), redraws the MNIST/CIFAR training curves as native pgfplots (vector, regenerable from logs/), and adds a BatchNorm "why normalizing helps" intuition.

The v0.5.7 headline still holds: two parallel-agent audits closed. The "canonical correct := rfl" pattern at non-smooth operators (ReLU, the composed MLP, MaxPool2) now has machine-checked smooth-point bridges: relu_codegen_matches_canonical and maxPool2_codegen_matches_canonical prove the canonical-witness backward equals the codegen formula wherever every coordinate avoids the kink. A HasVJPAt pointwise framework provides smooth-input variants of the three kinked-operator instances whose correct field is a real chain-rule proof rather than rfl. The comparator suite extends from 38 → 41 theorems independently kernel-rechecked against `[propext, Quot.sound, Classical.choice]`. Blueprint gets a half-dozen flow improvements (GAP defined at first material use in Ch 6, Diffusion split into its own Bestiary subsection, ResNet entry expanded to the full standard family including R-18, Tomáš Skřivan's Scientific Computing in Lean credited at the top of the acknowledgments). Android bottom-cutoff bug fixed (issue #2); Umami cookieless analytics replaces planned GA. First Zenodo deposit lands with this release.

The v0.5.6 headline still holds: Chapter 9 lands its ConvNeXt-T worked example (84.94% val on Imagenette, paper-faithful recipe); Chapter 10 gets a Data Augmentation section with a 9-row ViT recipe ablation table — CutMix is the load-bearing knob at 9.5K images, and stacking RandAugment + Random Erasing on top of it hurts val accuracy. Bestiary gets paper-exact entries for VGG, ResNet-50/101/152, WRN, and DenseNet, plus the "N new primitives" claim reframed around the Ch 2-10 reader's toolbox (what's free) rather than the codebase (what's already in Types.lean). Found and fixed a long-standing eval-pipeline bug along the way: centerCrop was running on already-224 val data, reading past per-image bounds and making heavy-aug runs appear to collapse. New LEAN_MLIR_EVAL_ONLY=1 mode re-evals saved checkpoints in ~5 sec each.

The v0.5.5 headline still holds: Swish/SiLU as a first-class activation (forward + backward + proved swish_has_vjp_correct) plus the independent-kernel comparator re-check covering 38 theorems via public *_has_vjp_correct wrappers, and Ch 2's "Why VJPs, not Jacobians?" bridge + canonical-pdiv witness explainer + three-pillar TikZ spine diagram.

On top of that, a differential-test suite in tests/vjp_oracle/ uses JAX's value_and_grad as an oracle for the hand-derived VJPs in LeanMlir/Proofs/. Nine test cases cover every axiom family — dense, conv, BN, maxPool, residual (biPath), depthwise, SE (elementwise product), attention, and the transformer block — each verified to 1–2 ULP of JAX autodiff. The ULP-floor cross-backend agreement (Lean→IREE→GPU vs Lean→JAX→XLA on both NVIDIA and AMD) established in v0.5.4 still holds; see traces/CROSS_BACKEND_RESULTS.md for the four-corner verification tables.