I may be misunderstanding you, but I think our point of confusion/disagreement is that you're still reading them as talking about how Lean proofs are created, whereas, given the context, I'm confident they were talking about how Lean proofs are reviewed (after being created by a human or LLM).

I hope there's no hard feelings, by the way -- I wasn't meaning to be nasty to you in that comment. I guess I thought your reading was a bit uncharitable, but I understand that misunderstandings happen (very much including on my end) and I didn't mean to make a big thing of it, so I'm sorry if I came across rudely.