Numerical packages in lean numlean lean karray

Webserver example. Custom syntax https://github.com/leanprover/lean4/blob/master/tests/playground/webserver/Webserver.lean

novice friendly induction tactic https://arxiv.org/pdf/2012.08990.pdf

metaprogramming framework for formal verification https://dl.acm.org/doi/pdf/10.1145/3110278

http://leanprover.github.io/papers/lean4.pdf lean4

“The Lean typeclass resolution procedure can be viewed as a simple λ-Prolog interpreter [8], where the Horn clauses are the user declared instances.” That sounds fun

Build

elan tool

leanpkg

lake is a new build tool on the horizon

Using nix is kind of a pain. I haven’t done it.