Because proofs are entirely finitary, whereas truth in a structure is not, it is common for work in constructive mathematics to emphasize provability. The relationship between provability in classical (or nonconstructive) systems and provability in intuitionistic (or constructive, respectively) systems is of particular interest. Results such as the [[Gödel–Gentzen negative translation]] show that it is possible to embed (or ''translate'') classical logic into intuitionistic logic, allowing some properties about intuitionistic proofs to be transferred back to classical proofs.
Recent developments in proof theory include the study of [[proof mining]] by [[Ulrich Kohlenbach]] and the study of [[proof-theoretic ordinal]]s by Michael Rathjen.
==Connections with computer science==