Lean is a currently-niche programming language / proof-assistant. A proof assistant is basically a tool to construct mathematical proofs, which verifies that the proofs are correct like how a compiler verifies types in your programs.

IIUC a regular programming language with a certain set of restrictions already duals as a proof-assistant as discovered by Curry & Howard. By restrictions, I mean something like how Rust forces you to follow certain rules compared to Java.