Comment by xrisk

Can you give some context on how using Lean benefits?

In my understanding, proofs are usually harder to transcribe into Lean which is nobody _writes_ proofs using Lean.

What is a nlinarith?