| Publication | Date of Publication | Type |
|---|
| Algorithmic barriers to representing conditional independence | 2024-12-19 | Paper |
| A proof-producing compiler for blockchain applications | 2024-11-26 | Paper |
| Certified knowledge compilation with application to verified model counting | 2024-11-26 | Paper |
| What we talk about when we talk about mathematics | 2024-10-24 | Paper |
| Mathematics and language | 2024-09-06 | Paper |
| Verified reductions for optimization | 2024-04-05 | Paper |
| 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 |
| Book review of: S. B. Cooper (ed.) and J. van Leeuwen (ed.), Alan Turing. His work and impact | 2016-06-15 | Paper |
| A heuristic prover for real inequalities | 2016-05-26 | Paper |
| Book review of: T. C. Hales, Dense sphere packings. A blueprint for formal proofs | 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 |
| Understanding, formal verification, and the philosophy of mathematics | 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 |
| Update procedures and the 1-consistency of arithmetic | 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 |
