Comment by baq

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.