| Maintaining a library of formal mathematics F van Doorn, G Ebner, RY Lewis International Conference on Intelligent Computer Mathematics, 251-267, 2020 | 30 | 2020 |
| Formalizing the Solution to the Cap Set Problem SR Dahmen, J Hölzl, RY Lewis arXiv preprint arXiv:1907.01449, 2019 | 23 | 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 | 17 | 2019 |
| A heuristic prover for real inequalities J Avigad, RY Lewis, C Roux Journal of Automated Reasoning 56, 367-386, 2016 | 17 | 2016 |
| An extensible ad hoc interface between Lean and Mathematica RY Lewis arXiv preprint arXiv:1712.09288, 2017 | 14 | 2017 |
| Formalizing the ring of Witt vectors J Commelin, RY Lewis Proceedings of the 10th ACM SIGPLAN International Conference on Certified …, 2021 | 12 | 2021 |
| Simplifying Casts and Coercions RY Lewis, PN Madelaine PAAR 2020: Seventh Workshop on Practical Aspects of Automated Reasoning, 53-62, 2020 | 12 | 2020 |
| Logic and proof J Avigad, RY Lewis, F van Doorn Version f8e30b0, Released under Apache 2, 2017 | 6 | 2017 |
| A bi-directional extensible interface between Lean and Mathematica RY Lewis, M Wu Journal of Automated Reasoning, 1-24, 2022 | 5 | 2022 |
| Polya: a heuristic procedure for reasoning with real inequalities RY Lewis MS thesis, Department of Philosophy, Carnegie Mellon University, 2014 | 4 | 2014 |
| Automation and computation in the Lean theorem prover RY Lewis, L de Moura Talk at HaTT, 2016 | 3 | 2016 |
| The Lean mathematical library T Community" 9th ACM SIGPLAN International Conference on Certified Programs and Proofs …, 2020 | 2* | 2020 |
| Formalized functional analysis with semilinear maps F Dupuis, RY Lewis, H Macbeth arXiv preprint arXiv:2202.05360, 2022 | 1 | 2022 |
| Two Tools for Formalizing Mathematical Proofs RY Lewis PhD thesis, Carnegie Mellon University, 2018 | 1 | 2018 |
| 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 |
| Energy-minimizing unit vector fields Y Digilov, W Eggert, R Hardt, J Hart, M Jauch, R Lewis, C Loftis, A Mehta, ... Involve, a Journal of Mathematics 3 (4), 435-450, 2011 | | 2011 |
| Complex Analysis and Cauchy’s Integral Theorem in Lean RY Lewis, JC Blanchette | | |
