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.