Robert Y. Lewis

Robert Y. Lewis is a Lecturer in the Department of Computer Science at Brown University. His work focuses on formal methods and verification, logic, and the foundations of mathematics, as well as their applications in computer science and mathematics education. Prior to joining Brown, he was a postdoc at the Vrije Universiteit Amsterdam and earned his PhD in Pure and Applied Logic at Carnegie Mellon University. Earlier, he taught high school mathematics at St. Agnes Academy in Houston.

Research Interests: Lewis specializes in interactive theorem proving, automated reasoning, and type theory. His research bridges formal mathematics with computational tools, emphasizing proof assistants like Lean and their integration with other systems such as Mathematica. He is also involved in mathematics education, particularly through open-source course development.

Publications: His recent work includes formalizing mathematical structures (e.g., Witt vectors, p-adic integers), developing proof assistant interfaces, and advancing automated reasoning techniques. Projects span both foundational mathematics and practical tools for formal verification.