Erdős problem #870 solved with ChatGPT-5.5-Pro and Leantwitter.com3 points·by asparagui·vor 15 Tagen·0 comments
Show HN: Verified Deep Learning with Lean 4brettkoonce.github.io6 points·by asparagui·vor 3 Monaten·0 comments
DJI is >96% of RemoteID usage in the US [video]youtube.com4 points·by asparagui·vor 4 Monaten·0 comments
Towards Robust Mathematical Reasoning [pdf]aclanthology.org1 points·by asparagui·vor 8 Monaten·0 comments
asparagui·vor 26 Tagen·discussBeen formalizing the math of deep learning in Lean 4 by lowering to MLIR/IREE.https://github.com/brettkoonce/lean4-mlir
asparagui·vor 2 Monaten·discusshttps://brettkoonce.github.io/lean4-mlir/blueprint/https://github.com/brettkoonce/lean4-mlirI (w/ Claude) have built a framework for writing neural networks in Lean 4 that compiles to StableHLO MLIR and runs on GPU via IREE.
asparagui·vor 2 Monaten·discussI was going to call my project that but Claude said that wasn't professional. rip "a delightful mixture of lean"
asparagui·vor 5 Monaten·discussNo, DJI is going to be banned in the US going forward (geopolitics). I am building a NDAA-compliant stack!
https://github.com/brettkoonce/lean4-mlir