A formal type of proof most frequently encountered in elementary geometry courses in which known or derived statements are written in the left column, and the reason that each statement is known or valid is written next to it in the right column. The proof then proceeds from the known facts to the theorem to be demonstrated. […] However, this form of proof is virtually never used by practicing mathematicians because its confining and verbose format render it of very limited utility to any but the most simple of theorems.

Hmm, maybe this is why people don’t like Lean LOL.