[Matryoshka-devel] New Matryoshka member: Johannes Hölzl

Jasmin Blanchette jasmin.blanchette at inria.fr
Wed Nov 23 17:34:23 CET 2016

Dear colleagues,

It is my pleasure to announce that Johannes Hölzl, currently at the TU Münich (in Tobias Nipkow's group) and soon at Carnegie Mellon (in Jeremy Avigad's group), will join Matryoshka as a postdoc in Amsterdam starting in fall 2017. Johannes will bring his ample expertise formalizing math in Isabelle and (by then) Lean to the project. He will probably end up working on many different aspects of the project, all the way from the heuristics to the hammers, with a likely detour through superposition; and those of us who formalize metatheory will surely benefit from his expertise too.

His initial appointment will be for two years. The formalities are underway, but I doubt the scientific council of VU Amsterdam will cause any trouble with such a prolific researcher and formalizer:




More information about the matryoshka-devel mailing list