Comment by galaxyLogic

> Mathlib, the dominant Lean library, is a human-curated formalization of an ever-growing fraction of existing human mathematics.

So why don;t they use AI to write Lean programs? That should make the AI-proofs more readily human undersrndable.