[prplfsh]

It's my own ignorance speaking, but is this as true in math? I could see this being a problem for programs where you have few, if any, real axioms and the axioms themselves change. But if we're talking math, the axioms should be fixed.

[smj-edison]

Most math does proofs somewhat informally (as in the proofs are written in a conversational style, and they're considered valid when they convince the majority of mathemeticians), but those proofs can be traced back to ZFC (a specific formulation of set theory and first order logic).

Type theory, especially dependant types, are a pretty recent development, and aren't really used in practice in math. Even in Mathlib (what most people mean when they say they've used lean), they encode first order logic. The proofs are dependently typed, but the actual logic of the proof is all in ZFC.