Comment by baq
19 hours ago
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.
19 hours ago
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.
Mathematicians care about interesting ideas, not whether their theorems are true :-)
They care about if it’s true. But the role of the formal proof is a kind of spell checker or static analysis after they have the idea.
4 replies →