Can all classical math proofs be represented in type theory? Posted by Programmer2134, at math.stackexchange.com, 14 Jul 2018 The curry howard isomorphism states that proofs in intuitionist logic can be represented as terms, and theorems as types. …