| Publication | Date of Publication | Type |
|---|
Carleson Operators on Doubling Metric Measure Spaces
(available as arXiv preprint) | N/A | Paper |
| Integrals within integrals: a formalization of the Gagliardo-Nirenberg-Sobolev inequality | 2026-02-10 | Paper |
A blueprint for the formalization of norm-variation of multiple ergodic averages for commuting transformations
(available as arXiv preprint) | 2026-01-01 | Paper |
Formalizing Carleson's Theorem in Lean
(available as arXiv preprint) | 2026-01-01 | Paper |
Carleson operators on doubling metric measure spaces
(available as arXiv preprint) | 2025-01-01 | Paper |
The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale
(available as arXiv preprint) | 2025-01-01 | Paper |
Formalized Haar Measure
(available as arXiv preprint) | 2023-06-20 | Paper |
scientific article; zbMATH DE number 7649968 (Why is no real title available?)
(available as arXiv preprint) | 2023-02-03 | Paper |
| Designing a general library for convolutions | 2022-10-14 | Paper |
| Formalising the h-principle and sphere eversion | 2022-10-14 | Paper |
Designing a general library for convolutions
(available as arXiv preprint) | 2022-01-01 | Paper |
Formalising the $h$-principle and sphere eversion
(available as arXiv preprint) | 2022-01-01 | Paper |
| A Formal Proof of the Independence of the Continuum Hypothesis | 2021-02-04 | Paper |
Sequential colimits in homotopy type theory
Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-21 | Paper |
Maintaining a library of formal mathematics
(available as arXiv preprint) | 2021-01-20 | Paper |
Higher groups in homotopy type theory
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science | 2021-01-20 | Paper |
A Formal Proof of the Independence of the Continuum Hypothesis
(available as arXiv preprint) | 2021-01-01 | Paper |
A formalization of forcing and the unprovability of the continuum hypothesis
(available as arXiv preprint) | 2019-04-23 | Paper |
| On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory | 2018-08-31 | Paper |
Homotopy type theory in Lean
(available as arXiv preprint) | 2018-01-04 | Paper |
Higher Groups in Homotopy Type Theory
(available as arXiv preprint) | 2018-01-01 | Paper |
On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory
(available as arXiv preprint) | 2018-01-01 | Paper |
| Constructing the Propositional Truncation using Non-recursive HITs | 2015-12-07 | Paper |
The Lean theorem prover (system description)
Automated Deduction - CADE-25 | 2015-12-02 | Paper |
| Propositional Calculus in Coq | 2015-03-30 | Paper |
Propositional Calculus in Coq
(available as arXiv preprint) | 2015-01-01 | Paper |
Constructing the Propositional Truncation using Non-recursive HITs
(available as arXiv preprint) | 2015-01-01 | Paper |
The structural theory of pure type systems
Lecture Notes in Computer Science | 2014-07-24 | Paper |
