citation needed, Tao certainly is on record using Lean and that carries some weight.

also, https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... i.e. there's no reason it should be as you say.

The link is exactly what I’m saying. I only hear cs people talk about it.

For mathematicians a proof is a means to an end, or a medium of expression - they care about what they say and why.

The correspondence isn’t about C programs corresponding to proofs in math papers. It’s a very a specific claim about kinds of formal systems which don’t resemble how math or programming is done.