Follow
Robert Y. Lewis
Robert Y. Lewis
Verified email at brown.edu - Homepage
Title
Cited by
Cited by
Year
Maintaining a library of formal mathematics
F van Doorn, G Ebner, RY Lewis
International Conference on Intelligent Computer Mathematics, 251-267, 2020
302020
Formalizing the Solution to the Cap Set Problem
SR Dahmen, J Hölzl, RY Lewis
arXiv preprint arXiv:1907.01449, 2019
222019
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
182019
A heuristic prover for real inequalities
J Avigad, RY Lewis, C Roux
Journal of Automated Reasoning 56, 367-386, 2016
172016
An extensible ad hoc interface between Lean and Mathematica
RY Lewis
arXiv preprint arXiv:1712.09288, 2017
142017
Formalizing the ring of Witt vectors
J Commelin, RY Lewis
Proceedings of the 10th ACM SIGPLAN International Conference on Certified …, 2021
122021
Simplifying Casts and Coercions
RY Lewis, PN Madelaine
PAAR 2020: Seventh Workshop on Practical Aspects of Automated Reasoning, 53-62, 2020
112020
Logic and proof
J Avigad, RY Lewis, F van Doorn
Version f8e30b0, Released under Apache 2, 2017
62017
A bi-directional extensible interface between Lean and Mathematica
RY Lewis, M Wu
Journal of Automated Reasoning, 1-24, 2022
52022
Polya: a heuristic procedure for reasoning with real inequalities
RY Lewis
MS thesis, Department of Philosophy, Carnegie Mellon University, 2014
42014
Automation and computation in the Lean theorem prover
RY Lewis, L de Moura
Talk at HaTT, 2016
32016
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
12022
Two Tools for Formalizing Mathematical Proofs
RY Lewis
PhD thesis, Carnegie Mellon University, 2018
12018
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
The system can't perform the operation now. Try again later.
Articles 1–19