Ask HN: Lean for Machine Learning?
JAX kinda excels at tracing python functions into jaxpr then into XLA because of the pure function assumption JAX has made.
How about using Lean, the dependently typed language. I know this might hinder speed of coding, but what if? Not just for deep learning but ML.
What if we write graph networks and graph updates through Lean or so on. Could there be any upsides with using Lean for ML? (The downsides are kinda obvious, so let’s maybe talk about possible up sides)
I heard some research group is trying to add type theory into deep learning through category theory, but i’m unsure of how that’s going and if this question might be related to that.
Do you think there is any benefit in using Lean for ML research?