Thibault Gauthier

portrait

I am working as a researcher at the Czech Technical Unversity in Prague with Josef Urban.
I am interested in interactive theorem proving and machine learning.

Publications

PhD Thesis

Projects

I actively develop for the HOL4 proof assistant:
     the tactical prover TacticToe,
     the integration of external provers via HolyHammer and
     a deep reinforcement learning framework based on tree neural networks and Monte Carlo tree search.

Contact

email: email@thibaultgauthier.fr
address:
Czech Institute of Informatics, Robotics, and Cybernetics
Czech Technical University in Prague
Zikova 4
166 36 Prague 6
Czech Republic