Every story and comment from the Hacker News API, in a layout borrowed from 2001.
A comment on Functional Programming in Lean – a book on using Lean 4 to write programs. Parent comment
I was stunned when I discovered it, because it does exactly what its name suggests: it's a huge library of math proofs available as a library in Lean.
There are no comments on this comment yet.
I was stunned when I discovered it, because it does exactly what its name suggests: it's a huge library of math proofs available as a library in Lean.