https://brettkoonce.github.io/lean4-mlir/blueprint/

https://github.com/brettkoonce/lean4-mlir

I (w/ Claude) have built a framework for writing neural networks in Lean 4 that compiles to StableHLO MLIR and runs on GPU via IREE.