Henryk Michalewski

University of Warsaw H.Michalewski@mimuw.edu.pl
2 Banacha St. +48 669 669 860
Warsaw, Poland office 1560


Habilitation in computer science, University of Warsaw. Title: Investigations of automata and related logics using methods of set theory.
Winter 2002
internship in the Fields Institute, Toronto, Canada, applications of set theory in other areas of mathematics
PhD in Mathematics, University of Warsaw Thesis title: Function spaces with topology of pointwise convergence
MA in Mathematics, University of Warsaw

Work Experience

Visiting Professor at Google (Staff Visiting Faculty Researcher at Google)
Visiting Professor at the Department of Computer Science of the University of Oxford
Assistant Professor at the Mathematical Institute of Polish Academy of Sciences
Invited Professor at the École normale supérieure de Lyon
research and business projects with deepsense.ai related to machine learning
Assistant Professor at the Mathematical Institute of Polish Academy of Sciences
Assistant Professor at the Department of Mathematics, Informatics and Mechanics of the University of Warsaw
Postdoc at the Department of Mathematics of the Ben Gurion University, Israel. Working on topics related to logic and foundations of mathematics
Teaching Assistant at the Department of Mathematics, Informatics and Mechanics of the University of Warsaw

Research interestes

My Masters and PhD theses concerned mathematical logic and games. Representative papers are Game-theoretic approach to the hereditary Baire property of Cp(NF) and Condensation of projective sets onto compacta. The importance of games in set theory is linked to the set-theoretical notion of descriptive complexity of sets. Namely, many classes of sets can be characterized using so called game quantifiers. With such a quantifier applied to a parametrized family of two-person games we can select parameters where the first player has a winning strategy.

In my Habilitation I turned to the theory of automata on trees, which plays a fundamental role in computer science, applying ideas from game quantification. Measure Properties of Game Tree Languages proved that sets defined by automata on trees correspond to sets defined with game quantifiers over games with universes being boolean combinations of Fσ sets. This is useful since Kolomogorov proved that such sets are tame in several senses -- for example, they are Lebesgue measurable. In On the Decidability of MSO+U on Infinite Trees we combined definability arguments with prior undecidability results to show the first undecidability result for a logic on trees, MSO+U. How unprovable is Rabin's decidability theorem? dealt with the interaction of automata theory and proof theory; the paper provides a fine-grained analysis of the axioms needed to prove a fundamantal decidability results in automata and logic, Rabin's theorem.

From logic, automata, and the theory of general games, I turned to the practice of games in the usual human sense. In 485 - a new upper bound for Morpion Solitaire we reduced the problem of finding the upper bound in the Morpion Solitaire game to a number of linear optimization tasks, which are amenable to computational solutions. This was my entry point into AI, and led to a series of papers on Atari games and Deep Reinforcement learning, including Learning from the memory of Atari 2600, Hierarchical Reinforcement Learning with Parameters, Reinforcement learning of theorem proving, Neural heuristics for SAT solving Towards Finding Longer Proofs. In 2018 I have started a business collaboration with Volkswagen which resulted in an experiment Simulation-based reinforcement learning for real-world autonomous driving - we have trained our agents in simulation and tested on a full-size passenger vehicle.

Doctoral students

Grants and projects

Prizes, invited talks


Educational Projects

Program Committees