[Matryoshka-devel] New Matryoshka member: Rob Lewis

Jasmin Blanchette jasmin.blanchette at inria.fr
Fri Dec 16 23:18:58 CET 2016

Dear colleagues,

It is my pleasure to announce that Rob Lewis, currently at CMU (in Jeremy Avigad's group), will join Matryoshka as a postdoc in Amsterdam. He is expected to start in January 2018, once he has submitted his Ph.D. Rob will bring considerable expertise on the Lean prover, as a developer and user. He is one of the authors of Polya, a really neat heuristic prover for real inequalities that he is now integrating in Lean, with proof reconstruction. He has also worked on an integration of Lean and Mathematica, and he formalized the reals in Lean. Like Johannes, he is likely to end up contributing to many different aspects of the project, including an integration with his favorite proof assistant.

Since Lean shares many of the same goals as Matryoshka ("richer automatic provers; more automatic proof assistants; trustworthy theorems"), I trust we will find meaningful ways to collaborate. According to Jeremy Avigad, "World domination is just around the corner."

Rob's appointment will be for 2.5 years. The formalities are underway, but I doubt the "wetenschapscommissie" at VU Amsterdam will cause any trouble with such a qualified researcher:


The first signs from Amsterdam were positive: "Rob Lewis is duidelijk een ijzersterke kandidaat, je hebt heel snel een prachtig team op Matryoshka vergaard."



More information about the matryoshka-devel mailing list