Comment by FrustratedMonky

Not a mathematician. Why not just always use LEAN? Why use natural language at all?