oh yep, it's definitely more than usable for 'actual programming' beyond just maths proofs. Things like: - bindings to godot (https://github.com/kiranandcode/

oh yep, it's definitely more than usable for 'actual programming' beyond just maths proofs. Things like: - bindings to godot (https://github.com/kiranandcode/lean4-godot https://github.com/kiranandcode/lean4-godot) - advent of code (https://github.com/kiranandcode/lean-aoc https://github.com/kiranandcode/lean-aoc) - ffi bindings to constraint solvers (https://github.com/kiranandcode/cleango/ https://github.com/kiranandcode/cleango/) Obviously a slightly biased selection here, but the key point is to clarify that it's more than feasible to use it for real programs that do all sorts of non-mathy stuff.