The aim of this thesis is to provide an introductory discussion of the two most common modern foundations of mathematics: axiomatic set theory and dependent type theory. To provide a basis, we begin by explaining the main concepts of and motivations for the respective systems in their standard formulation. This includes a brief outline of first-order logic and ZF set theory on the one side, and of simply typed lambda calculus and Martin-Lof type theory on the other side. Subsequently sketching an ongoing debate, both approaches are compared with respect to general criteria for practicality, their respective philosophical justification, and their approximate consistency strength. We argue that, despite being similarly expressive for the purposes of formal mathematics, dependent type theory is based on the more convincing constructivist view and advantageous for computer-assisted proving. To illustrate its potential for modern applications, some parts of the mathematical development are formally verified using the Coq proof assistant.