A Heuristic Prover for Real Inequalities. - Jeremy Avigad; Robert Y. Lewis; Cody Roux (J. Autom. Reason., 2016)

An Extensible Ad Hoc Interface between Lean and Mathematica. - Robert Y. Lewis (PxTP, 2017)

A formal proof of hensel's lemma over the p-adic integers. - Robert Y. Lewis (CPP, 2019)

Formalizing the Solution to the Cap Set Problem. - Sander R. Dahmen; Johannes Hölzl; Robert Y. Lewis (ITP, 2019)

Simplifying Casts and Coercions (Extended Abstract). - Robert Y. Lewis; Paul-Nicolas Madelaine (PAAR+SC²@IJCAR, 2020)

Maintaining a Library of Formal Mathematics. - Floris van Doorn; Gabriel Ebner; Robert Y. Lewis (CICM, 2020)

Normalizing Casts and Coercions. - Robert Y. Lewis; Paul-Nicolas Madelaine (CoRR, 2020)

Formalizing the ring of Witt vectors. - Johan Commelin; Robert Y. Lewis (CPP, 2021)

A Bi-Directional Extensible Interface Between Lean and Mathematica. - Robert Y. Lewis; Minchao Wu (J. Autom. Reason., 2022)

Formalized Functional Analysis with Semilinear Maps. - Frédéric Dupuis; Robert Y. Lewis; Heather Macbeth (J. Autom. Reason., 2024)