Carnegie Mellon University

January 14, 2016

# Graduate Student Profile: Rob Lewis

Rob, a Ph.D. student in Pure and Applied Logic, came to CMU in August 2012 and has been working hard ever since on projects involving computers and mathematics. Get to know all about him!

Where are you from originally? What brought you to CMU?
I grew up in Boston, did my undergrad in Houston, and taught high school math for two years in Houston before moving here. I was a double major in math and philosophy as an undergrad, and CMU's program combined the two subjects in a way that I liked.

Tell us about your research and what your focusing on here. What projects have you been working on, with whom?
Broadly, I work on topics involving computers in mathematics. There are a few directions to this work. For one, you can use computers to verify mathematical arguments; that is, to check that a proof written by a human is logically correct. For another, you can use computers to find mathematical objects, or check that certain properties hold of certain objects. For one more, you can use computers to generate proofs on their own. This is similar to the second point, but instead of just confirming that an object has a property for instance, the computer produces an argument for why that's the case.

My master’s project fell into the second category. My advisor (Jeremy Avigad) and I developed a system - called Polya - that will try to determine if a set of inequalities has no solution. Lots of geometrical and physical problems can be stated in this form, and these problems can be very difficult to solve algorithmically. Polya differs from other systems in that it uses "human-like" heuristics to try and find simple solutions, instead of brute force.

I've also been working on the Lean theorem prover, a new system under development at Microsoft Research. Lean combines the first and third categories above. It's an environment for verifying proofs written by humans, that has/will have many automated tools available to help. There are a number of people around the world working on this project, including Leonardo de Moura (the developer at Microsoft Research), Jeremy Avigad, Floris van Doorn (another Philosophy department graduate student), and Soonho Kong (a CMU computer science graduate student).

What are your future plans and goals?
I hope to get a job in academia -- I enjoy both teaching and research, and would like to keep doing both.

When you’re not teaching and researching, what are your hobbies and interests?
In theory: reading, biking, building things. In practice: sleeping.