RE: https://mathstodon.xyz/@proofsandprompts/117581938581433669

This. Filippo, in an ode to the mathlib community and the formalisation community in general (not just in Lean), also address the paradoxical pressures against understanding in the pursuit of prestige, i.e. the mathematical publishing industry.