15 citations · 42 across the 8 of their papers we have counts for
9 papers
Formalized functional analysis with semilinear maps
Frédéric Dupuis, Robert Y. Lewis, Heather Macbeth
Semilinear maps are a generalization of linear maps between vector spaces where we allow the scalar action to be twisted by a ring homomorphism such as complex conjugation. In part…
A bi-directional extensible interface between Lean and Mathematica
Robert Y. Lewis, Minchao Wu
We implement a user-extensible ad hoc connection between the Lean proof assistant and the computer algebra system Mathematica. By reflecting the syntax of each system in the other…
Formalizing the Ring of Witt Vectors
Johan Commelin, Robert Y. Lewis
The ring of Witt vectors over a base ring is an important tool in algebraic number theory and lies at the foundations of modern -adic Hodge theory. $\mathbb{W…
Maintaining a Library of Formal Mathematics
Floris van Doorn, Gabriel Ebner, Robert Y. Lewis
The Lean mathematical library mathlib is developed by a community of users with very different backgrounds and levels of experience. To lower the barrier of entry for contributors…
Simplifying Casts and Coercions
Robert Y. Lewis, Paul-Nicolas Madelaine
This paper introduces norm_cast, a toolbox of tactics for the Lean proof assistant designed to manipulate expressions containing coercions and casts. These expressions can be frust…
A formal proof of Hensel's lemma over the p-adic integers
Robert Y. Lewis
The field of -adic numbers and the ring of -adic integers are essential constructions of modern number theory. Hensel's lemma, described by Gouv…
Formalizing the Solution to the Cap Set Problem
Sander R. Dahmen, Johannes Hölzl, Robert Y. Lewis
In 2016, Ellenberg and Gijswijt established a new upper bound on the size of subsets of with no three-term arithmetic progression. This problem has received much m…
An Extensible Ad Hoc Interface between Lean and Mathematica
Robert Y. Lewis
We implement a user-extensible ad hoc connection between the Lean proof assistant and the computer algebra system Mathematica. By reflecting the syntax of each system in the other…
A heuristic prover for real inequalities
Jeremy Avigad, Robert Y. Lewis, Cody Roux
We describe a general method for verifying inequalities between real-valued expressions, especially the kinds of straightforward inferences that arise in interactive theorem provin…