I read this Quanta article this morning: https://www.quantamagazine.org/why-mathematical-proof-is-a-social-compact-20230831/

I want to share some quick thoughts over my morning coffee.

I largely agree that a proof is a social construct---a conversation---but I see computation as an extra way to participate in and broaden the scope and trustworthiness of this social conversation. The conversation is now between not just humans but also computational tools that can assist at any step of the way. That can be hugely empowering if done right. (And hugely misleading if done poorly.)

Computation can also help with vetting the conversation. The whole point of proof assistants like Lean is to minimize the possible points of failure in the conversation. The only things that are trusted should be small and simple enough that a human can read and understand them---this is called the "de Bruijn criterion," and it is the philosophy behind the implementation of proof assistants like Lean.

It is also behind the ways the communities interact when using these tools. More time can be spent vetting the theorem statements and definitions, for example, when the actual proof is checked by a small trusted kernel (which is also vetted by humans).