Hacker GitHub

← All repos

brettkoonce/lean4-mlir

View on GitHub ↗ ★ 48 MLIR

Lean specification of neural architectures with verified GPU codegen.

4 mentions on Hacker News by 1 person: 1 story, 3 comments · first 2026-04-10 · latest 2026-10-20

Mentions per year 4 mentions · busiest year 2026 (4)
20082026
AllStoriesComments NewestTopOldest
  1. Very cool! I have been using Lean to drive PJRT like so: https://github.com/brettkoonce/lean4-mlir and in theory your code could unlock another platform!
    comment by asparagui · 2026-10-20 · in Google open-sources TorchTPU, a native PyTorch back end for TPUs
  2. Been formalizing the math of deep learning in Lean 4 by lowering to MLIR/IREE. https://github.com/brettkoonce/lean4-mlir
    comment by asparagui · 2026-06-15 · in Ask HN: What are you working on? (June 2026)
  3. 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.
    comment by asparagui · 2026-05-10 · in Ask HN: What are you working on? (May 2026)
  4. ▲ 5
    Image Recognition with Lean 4
    story by asparagui · 2026-04-10 · 0 comments