| The Lean theorem prover (system description) L De Moura, S Kong, J Avigad, F Van Doorn, J von Raumer Automated Deduction-CADE-25: 25th International Conference on Automated …, 2015 | 783 | 2015 |
| Higher groups in homotopy type theory U Buchholtz, F van Doorn, E Rijke Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer …, 2018 | 67 | 2018 |
| On the formalization of higher inductive types and synthetic homotopy theory F Van Doorn arXiv preprint arXiv:1808.10690, 2018 | 38 | 2018 |
| Maintaining a library of formal mathematics F van Doorn, G Ebner, RY Lewis International Conference on Intelligent Computer Mathematics, 251-267, 2020 | 37 | 2020 |
| Constructing the propositional truncation using non-recursive hits F Doorn Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and …, 2016 | 37 | 2016 |
| Homotopy type theory in Lean F van Doorn, J von Raumer, U Buchholtz Interactive Theorem Proving: 8th International Conference, ITP 2017 …, 2017 | 35 | 2017 |
| A formal proof of the independence of the continuum hypothesis JM Han, F van Doorn Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020 | 29 | 2020 |
| Explicit convertibility proofs in pure type systems F van Doorn, H Geuvers, F Wiedijk Proceedings of the Eighth ACM SIGPLAN international workshop on Logical …, 2013 | 21 | 2013 |
| Formalized Haar Measure F van Doorn arXiv preprint arXiv:2102.07636, 2021 | 13 | 2021 |
| Formalising the h-principle and sphere eversion F van Doorn, P Massot, O Nash Proceedings of the 12th ACM SIGPLAN International Conference on Certified …, 2023 | 12 | 2023 |
| Sequential colimits in homotopy type theory K Sojakova, F Doorn, E Rijke Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer …, 2020 | 11 | 2020 |
| A Formalization of Forcing and the Unprovability of the Continuum Hypothesis JM Han, F van Doorn arXiv preprint arXiv:1904.10570, 2019 | 7 | 2019 |
| Logic and proof J Avigad, RY Lewis, F van Doorn Version f8e30b0, Released under Apache 2, 2017 | 7 | 2017 |
| Propositional Calculus in Coq F van Doorn arXiv preprint arXiv:1503.08744, 2015 | 7 | 2015 |
| A formalization of forcing and the consistency of the failure of the continuum hypothesis J Han, F van Doorn International Conference on Interactive Theorem Proving. Springer, Heidelberg 10, 2019 | 6 | 2019 |
| The structural theory of pure type systems C Roux, F van Doorn International Conference on Rewriting Techniques and Applications, 364-378, 2014 | 6 | 2014 |
| Formalising the -principle and sphere eversion P Massot, F van Doorn, O Nash arXiv preprint arXiv:2210.07746, 2022 | 4 | 2022 |
| The sphere eversion project P Massot, O Nash, F van Doorn | 3 | 2024 |
| The Lean mathematical library mathlib Community. Proceedings of the 9th ACM SIGPLAN International Conference on Certified …, 2020 | 2 | 2020 |
| Carleson operators on doubling metric measure spaces L Becker, F van Doorn, A Jamneshan, R Srivastava, C Thiele arXiv preprint arXiv:2405.06423, 2024 | 1 | 2024 |
Jeremy AvigadProfessor of Philosophy and Mathematical Sciences, Carnegie Mellon UniversityVerified email at cmu.edu