15 citations · 34 across the 6 of their papers we have counts for
6 papers · 1 filter
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…
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…