Brown CS News

Click the link that follows for more news about our historic CS With Impact expansion.

A native of Boston, Robert Y. Lewis is returning to the northeast after three years in the Netherlands (“I’ve been biking a lot, maybe because of living there – it’s definitely a hobby”) and he joins Brown CS as lecturer this fall. He’s the latest hire in the multi-year CS With Impact campaign, the most significant expansion in the department’s history.

Rob likes to build. An amateur woodworker who picked up a few tricks from his father, he’s made his own furniture and what he describes as a few small trinkets. But he’s equally at home among the less concrete: “I use computers for proof-based math, which I had no idea was a thing until I met my dissertation advisor. It was this sudden realization – I feel like nobody thinks of computers being applied to math in this ‘wrong way,’ for interactive theorem proving and automated reasoning.”

More on that later. Rob tells us that his first exposure to computer science was in high school, which had a “surprisingly comprehensive” curriculum for the time. After a year of tutorials and instruction, sophomores were turned loose to write code. It was a great way, he says, to see the possibilities of CS, decide what you want to do, and then figure out how to do it. For Rob, math was an obvious application, but along more traditional lines. The idea that you could use computers to interactively prove theorems wasn’t yet on his radar.

“I can’t say that I had much of a plan as I started college,” says Rob. “I knew I wanted to major in math, and Rice is similar to Brown in that it’s very easy to pick up a double major. I took some psychology, and philosophy really appealed to me – there are connections between philosophy and the foundations of math that aren’t really obvious on the surface.”

Teaching beckoned, but two years as a high school math teacher convinced Rob that K-12 education wasn’t the right setting. But computer science had begun to enter the picture: first, two Master’s degrees from Carnegie Mellon University (Logic, Computation, and Methodology in 2014 and then Mathematics in 2015), and then a PhD with CMU’s program in Pure and Applied Logic. It provided a blend of philosophy, math, and CS, offering a chance to work with faculty from all three departments.  

It was also a sea-change in Rob’s outlook. “We think of computers doing math,” he says, “as carrying out repetitive tasks many times, using them to solve concrete instances of mathematical problems. But that’s not what most mathematicians do! They define precise abstract things, state their properties, and prove that the properties hold – and write these proofs in natural language. There’s nothing calculational about that most of the time. It was amazing to realize how computers could help us with this side of mathematics.”

Currently, Rob’s big research interest is an open-source library of formal mathematics called mathlib, in a language called Lean, that just broke a half-million lines of code. “If you want to formalize a certain area of math,” he says, “it lets you just type in your statements, your proofs, and then the system checks that they’re complete according to a certain logic.” 

“Right now,” Rob says, “I’m looking for hard things to do – pushing the boundaries of the system, making it easier for people to see how they can use computers to do a much broader range of things.”

Formal methods, he says, are more accessible than they were not so long ago: “Lean began in 2013, and a big motivation was to address usability issues. Software has been everywhere for a long time, and we’re really seeing the cost of having major issues in a release. If FM becomes widespread, the hope is that the layperson notices nothing but that everything works smoother: no flashing signs that software is verified, but fewer hacks, fewer failures of critical systems. Lots of changes that would be visible if you knew where to look, but the average person won’t know.”

Kickstarting the formal methods undergraduate track is one of the things Rob is looking forward to most: “Brown CS has some FM classes now, but there are so many possibilities for reorganizing things and bulking up the curriculum. I’m going to be starting with a course on deductive reasoning – it’s the first in a new branch of possible courses, and I want to see where it’ll go. I’ve really conceived of it as an introduction to the practice and theory of proof of systems and deductive verification tools. The course will have three different sides, including the automation aspect, and I really want students to dig into the theoretical level: how these tools work, why give you a strong degree of certainty.”

Rob says that interactive theorem proving and automated reasoning appeal to him both because they’re a path less traveled and because they offer multidisciplinary possibilities. “There are research areas in any field where thousands of people worldwide are publishing variations on the same idea,” he explains. “When you take a multidisciplinary approach, you find people who have different training than you, different motivations. I like that about Brown and about the freedom given to students. I want them to try out weird combinations of different things and see what interests them. A big part of my projects is about getting things used. It’s hard to convince old mathematicians and old programmers that formal methods are important, so teaching is a good way to spread the gospel.”

Spreading the gospel, starting an open-source library with two people and having it grow to 20 maintainers and more than 150 contributors – is idealism at work? “I do think it’s idealistic,” Rob says, “but that’s part of the appeal. mathlib is very much a never-ending project. Our organizational approach might have to change at some point, but we’re keeping everyone working together. Surprisingly, it’s still pretty coherent and maintainable!” 

It seems like a balance of abstract and concrete again, the theoretical and the practical: “I didn’t get involved with mathlib with the intention of making it into a big open-source thing, but I became convinced that this model is the only way to do this specific project. I like how academia gives us the freedom to explore these wild tangents. A lot of this comes from my mathematical background – things with no obvious application, or maybe not for 100 years. Five years ago, people would have said that what I’m working on now is a weird academic tangent with no applications, but without academia pushing them forward, nobody in industry would have ever started using formal methods.”

For more information, click the link that follows to contact Brown CS Communication Outreach Specialist Jesse C. Polhemus.