Post

Although it started out as a theorem prover, Lean 4 is a general-purpose programming language that has the potential to challenge OCaml's `throne`.