Things like:
- bindings to godot (https://github.com/kiranandcode/lean4-godot)
- advent of code (https://github.com/kiranandcode/lean-aoc)
- ffi bindings to constraint solvers (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.