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.

> They care about if it’s true.

Not always.

If it is NOT true, they sometimes simply play "what if" and construct a new system where it could be true.

> If it is NOT true, they sometimes simply play "what if" and construct a new system where it could be true.

I trust you have some examples of this?

I think they're talking about conjectures that are unproven but seem "likely true" and people build further math off the assumption. E.G Reimann hypothesis

Complex numbers and Schwartz distributions (the thing the dirac delta is) come immediately to mind. “Not all numbers have square roots, but what if they did?” It seems like a common pattern.