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.

Projects
Most of my projects are integrated in HOL4.
Here is a demo of the tactical prover TacticToe.
tactictoe
Publications
Link
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