| Maintaining a library of formal mathematics F van Doorn, G Ebner, RY Lewis International Conference on Intelligent Computer Mathematics, 251-267, 2020 | 47 | 2020 |
| Formalizing the Solution to the Cap Set Problem SR Dahmen, J Hölzl, RY Lewis arXiv preprint arXiv:1907.01449, 2019 | 22 | 2019 |
| A formal proof of Hensel's lemma over the p-adic integers RY Lewis Proceedings of the 8th ACM SIGPLAN International Conference on Certified …, 2019 | 22 | 2019 |
| A heuristic prover for real inequalities J Avigad, RY Lewis, C Roux Journal of Automated Reasoning 56 (3), 367-386, 2016 | 20 | 2016 |
| Formalizing the ring of Witt vectors J Commelin, RY Lewis Proceedings of the 10th ACM SIGPLAN International Conference on Certified …, 2021 | 17 | 2021 |
| Mathematics in Lean J Avigad, K Buzzard, RY Lewis, P Massot Technical report, Lean community, 2020. En https://leanprover-community …, 2020 | 16 | 2020 |
| An extensible ad hoc interface between Lean and Mathematica RY Lewis arXiv preprint arXiv:1712.09288, 2017 | 15 | 2017 |
| Simplifying Casts and Coercions RY Lewis, PN Madelaine PAAR 2020: Seventh Workshop on Practical Aspects of Automated Reasoning, 53-62, 2020 | 12 | 2020 |
| A bi-directional extensible interface between Lean and Mathematica RY Lewis, M Wu Journal of Automated Reasoning, 1-24, 2022 | 10 | 2022 |
| Logic and proof J Avigad, RY Lewis, F van Doorn Version f8e30b0, Released under Apache 2, 2017 | 9 | 2017 |
| Formalized functional analysis with semilinear maps F Dupuis, RY Lewis, H Macbeth Journal of Automated Reasoning 68 (2), 1-26, 2024 | 6 | 2024 |
| The Lean mathematical library T Community" 9th ACM SIGPLAN International Conference on Certified Programs and Proofs …, 2020 | 5* | 2020 |
| Polya: a heuristic procedure for reasoning with real inequalities RY Lewis MS thesis, Department of Philosophy, Carnegie Mellon University, 2014 | 4 | 2014 |
| Two Tools for Formalizing Mathematical Proofs RY Lewis PhD thesis, Carnegie Mellon University, 2018 | 3 | 2018 |
| Automation and computation in the Lean theorem prover RY Lewis, L de Moura Talk at HaTT, 2016 | 3 | 2016 |
| KLean: Extending Operating System Kernels with Lean D Jin, E Lavi, J Jia, RY Lewis, N Vasilakis Proceedings of the 13th Workshop on Programming Languages and Operating …, 2025 | | 2025 |
| The Art of Formal Proof RY Lewis Math Horizons 32 (2), 20-23, 2024 | | 2024 |
| Normalizing Casts and Coercions RY Lewis, PN Madelaine arXiv preprint arXiv:2001.10594, 2020 | | 2020 |
| Toward AI for Lean, via metaprogramming RY Lewis AITP 2018, 2018 | | 2018 |
| A heuristic prover for real inequalities J Avigad, RY Lewis, C Roux Interactive Theorem Proving: 5th International Conference, ITP 2014, Held as …, 2014 | | 2014 |
