It's parroting proofs. This is no different than parroting a story.

https://lean-lang.org