| Publication | Date of Publication | Type |
|---|
| Mathematics and the formal turn | 2024-04-03 | Paper |
| TWO-SORTED FREGE ARITHMETIC IS NOT CONSERVATIVE | 2024-01-11 | Paper |
| An Impossible Asylum | 2023-05-11 | Paper |
| Reliability of mathematical inference | 2023-03-31 | Paper |
| Mathematical Logic and Computation | 2022-08-01 | Paper |
| Varieties of mathematical understanding | 2021-11-19 | Paper |
| Foundations | 2020-09-20 | Paper |
| MODULARITY IN MATHEMATICS | 2020-03-25 | Paper |
| Opinion: The Mechanization of Mathematics | 2018-11-02 | Paper |
| A formally verified proof of the central limit theorem | 2018-02-02 | Paper |
| On the computability of graphons | 2018-01-31 | Paper |
| Proof Theory | 2017-11-06 | Paper |
| Eliminating definitions and Skolem functions in first-order logic | 2017-06-13 | Paper |
| CHARACTER AND OBJECT | 2017-05-31 | Paper |
| Delta-Decidability over the Reals | 2017-05-16 | Paper |
| Logic's Lost Genius and Gentzen's Centenary | 2017-01-02 | Paper |
| Homotopy limits in type theory | 2016-07-27 | Paper |
| Alan Turing: His Work and Impact, A Book Review | 2016-06-15 | Paper |
| A heuristic prover for real inequalities | 2016-05-26 | Paper |
| Thomas Hales. Dense Sphere Packings: A Blueprint for Formal Proofs. Cambridge University Press, Cambridge, 2012, xiv + 271 pp. | 2016-03-18 | Paper |
| The Lean Theorem Prover (System Description) | 2015-12-02 | Paper |
| Oscillation and the mean ergodic theorem for uniformly convex Banach spaces | 2015-07-13 | Paper |
| A Heuristic Prover for Real Inequalities | 2014-09-08 | Paper |
| The concept of ``character in Dirichlet's theorem on primes in an arithmetic progression | 2014-07-01 | Paper |
| Ultraproducts and metastability | 2014-03-14 | Paper |
| Mathematics and language | 2013-10-04 | Paper |
| A Machine-Checked Proof of the Odd Order Theorem | 2013-08-07 | Paper |
| Uniform distribution and algorithmic randomness | 2013-04-23 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4904162 | 2013-01-28 | Paper |
| A metastable dominated convergence theorem | 2012-12-17 | Paper |
| Uncomputably noisy ergodic limits | 2012-11-23 | Paper |
| Algorithmic randomness, reverse mathematics, and the dominated convergence theorem | 2012-10-11 | Paper |
| δ-Complete Decision Procedures for Satisfiability over the Reals | 2012-09-05 | Paper |
| Inverting the Furstenberg correspondence | 2012-08-24 | Paper |
| Computability and analysis: the legacy of Alan Turing | 2012-06-15 | Paper |
| Zen and the art of formalisation | 2011-10-21 | Paper |
| The computational content of classical arithmetic | 2011-05-31 | Paper |
| https://portal.mardi4nfdi.de/entity/Q3079616 | 2011-03-02 | Paper |
| Metastability in the Furstenberg–Zimmer tower | 2011-01-11 | Paper |
| Local stability of ergodic averages | 2010-02-02 | Paper |
| A FORMAL SYSTEM FOR EUCLID’SELEMENTS | 2010-01-21 | Paper |
| Functional interpretation and inductive definitions | 2010-01-07 | Paper |
| The metamathematics of ergodic theory | 2009-03-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5421788 | 2007-10-24 | Paper |
| Combining decision procedures for the reals | 2007-10-11 | Paper |
| Automated Reasoning | 2007-09-25 | Paper |
| A decision procedure for linear ``big O equations | 2007-08-17 | Paper |
| Quantifier elimination for the reals with a predicate for the powers of two | 2007-02-26 | Paper |
| Mathematical method and proof | 2006-12-20 | Paper |
| Fundamental notions of analysis in subsystems of second-order arithmetic | 2006-04-28 | Paper |
| https://portal.mardi4nfdi.de/entity/Q5711876 | 2005-12-08 | Paper |
| Forcing in Proof Theory | 2005-05-24 | Paper |
| Number theory and elementary arithmetic† | 2004-06-10 | Paper |
| Transfer principles in nonstandard intuitionistic arithmetic | 2003-09-16 | Paper |
| AN ORDINAL ANALYSIS OF ADMISSIBLE SET THEORY USING RECURSION ON ORDINAL NOTATIONS | 2003-07-25 | Paper |
| Saturated models of universal theories | 2003-03-09 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4793022 | 2003-02-18 | Paper |
| https://portal.mardi4nfdi.de/entity/Q2776806 | 2002-07-22 | Paper |
| Algebraic proofs of cut elimination | 2002-05-21 | Paper |
| Interpreting classical theories in constructive ones | 2002-03-11 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4944901 | 2000-10-22 | Paper |
| Predicative functionals and an interpretation of \({\widehat{\text{ID}}_{<\omega}}\) | 1999-08-16 | Paper |
| The model-theoretic ordinal analysis of theories of predicative strength | 1999-06-29 | Paper |
| An effective proof that open sets are Ramsey | 1999-03-25 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4215634 | 1998-12-08 | Paper |
| https://portal.mardi4nfdi.de/entity/Q4375783 | 1998-07-08 | Paper |
| A Model-Theoretic Approach to Ordinal Analysis | 1997-11-05 | Paper |
| Formalizing forcing arguments in subsystems of second-order arithmetic | 1997-01-26 | Paper |
| On the relationship between ATR0 and | 1996-12-12 | Paper |
