Thibault Gauthier

Generating author description...

All published works

Action	Title	Year	Authors
+ PDF Chat	A Formal Proof of R(4,5)=25	2024	Thibault Gauthier Chad E. Brown
+ PDF Chat	Learning Guided Automated Reasoning: A Brief Survey	2024	Lasse Blaauwbroek David M. Cerna Thibault Gauthier Jan Jakubův Cezary Kaliszyk Martin Suda Josef Urban
+ PDF Chat	Learning Program Synthesis for Integer Sequences from Scratch	2023	Thibault Gauthier Josef Urban
+ PDF Chat	A Mathematical Benchmark for Inductive Theorem Provers	2023	Thibault Gauthier Chad E. Brown Mikoláš Janota Josef Urban
+	Alien Coding	2023	Thibault Gauthier Miroslav Olšák Josef Urban
+	A Mathematical Benchmark for Inductive Theorem Provers	2023	Thibault Gauthier Chad E. Brown Mikoláš Janota Josef Urban
+	Learning Program Synthesis for Integer Sequences from Scratch	2022	Thibault Gauthier Josef Urban
+	TacticToe: Learning to Prove with Tactics.	2021	Thibault Gauthier Cezary Kaliszyk Josef Urban Ramana Kumar Michael Norrish
+ PDF Chat	Learned Provability Likelihood for Tactical Search	2021	Thibault Gauthier
+	Learned Provability Likelihood for Tactical Search.	2021	Thibault Gauthier
+	Tree Neural Networks in HOL4	2020	Thibault Gauthier
+ PDF Chat	TacticToe: Learning to Prove with Tactics	2020	Thibault Gauthier Cezary Kaliszyk Josef Urban Ramana Kumar Michael Norrish
+ PDF Chat	Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic	2020	Thibault Gauthier
+	Tree Neural Networks in HOL4	2020	Thibault Gauthier
+	Self-Learned Formula Synthesis in Set Theory.	2019	Chad E. Brown Thibault Gauthier
+	Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic	2019	Thibault Gauthier
+	Learning from Tactic Steps in Formal Proofs	2019	Thibault Gauthier
+ PDF Chat	GRUNGE: A Grand Unified ATP Challenge	2019	Chad E. Brown Thibault Gauthier Cezary Kaliszyk Geoff Sutcliffe Josef Urban
+	Self-Learned Formula Synthesis in Set Theory	2019	Chad E. Brown Thibault Gauthier
+	Deep Reinforcement Learning for Synthesizing Functions in Higher-Order Logic	2019	Thibault Gauthier
+	Learning to Prove with Tactics	2018	Thibault Gauthier Cezary Kaliszyk Josef Urban Ramana Kumar Michael Norrish
+ PDF Chat	TacticToe: Learning to Reason with HOL4 Tactics	2018	Thibault Gauthier Cezary Kaliszyk Josef Urban
+	Sharing HOL4 and HOL Light proof knowledge	2015	Thibault Gauthier Cezary Kaliszyk
+	Premise Selection and External Provers for HOL4	2015	Thibault Gauthier Cezary Kaliszyk
+ PDF Chat	Sharing HOL4 and HOL Light Proof Knowledge	2015	Thibault Gauthier Cezary Kaliszyk
+	Sharing HOL4 and HOL Light proof knowledge	2015	Thibault Gauthier Cezary Kaliszyk
+	Matching concepts across HOL libraries	2014	Thibault Gauthier Cezary Kaliszyk
+	Matching concepts across HOL libraries	2014	Thibault Gauthier Cezary Kaliszyk
+ PDF Chat	Matching Concepts across HOL Libraries	2014	Thibault Gauthier Cezary Kaliszyk

Common Coauthors

Coauthor	Papers Together
Cezary Kaliszyk	13
Josef Urban	11
Chad E. Brown	6
Michael Norrish	3
Ramana Kumar	3
Mikoláš Janota	2
Geoff Sutcliffe	1
Jan Jakubův	1
Miroslav Olšák	1
David M. Cerna	1
Lasse Blaauwbroek	1
Martin Suda	1

Commonly Cited References

Action	Title	Year	Authors	# of times referenced
+ PDF Chat	Learning-Assisted Automated Reasoning with Flyspeck	2014	Cezary Kaliszyk Josef Urban	8
+	Premise Selection and External Provers for HOL4	2015	Thibault Gauthier Cezary Kaliszyk	7
+ PDF Chat	TacticToe: Learning to Reason with HOL4 Tactics	2018	Thibault Gauthier Cezary Kaliszyk Josef Urban	6
+ PDF Chat	Recycling Proof Patterns in Coq: Case Studies	2014	Jónathan Heras Ekaterina Komendantskaya	4
+ PDF Chat	Machine Learning in Proof General: Interfacing Interfaces	2013	Ekaterina Komendantskaya Jónathan Heras Gudmund Grov	4
+	Learning to Prove with Tactics	2018	Thibault Gauthier Cezary Kaliszyk Josef Urban Ramana Kumar Michael Norrish	3
+ PDF Chat	SEPIA: Search for Proofs Using Inferred Automata	2015	Thomas Gransden Neil Walkinshaw Rajeev Raman	3
+ PDF Chat	MizAR 40 for Mizar 40	2015	Cezary Kaliszyk Josef Urban	3
+ PDF Chat	Easy-First Dependency Parsing with Hierarchical Tree LSTMs	2016	Eliyahu Kiperwasser Yoav Goldberg	3
+	The Distance-Weighted k-Nearest-Neighbor Rule	1976	Sahibsingh A. Dudani	3
+ PDF Chat	Internal Guidance for Satallax	2016	Michael Färber Chad E. Brown	3
+ PDF Chat	The MMT API: A Generic MKM System	2013	Florian Rabe	2
+	Efficient Algorithms for Generating Elliptic Curves over Finite Fields Suitable for Use in Cryptography	2002	Harald Baier	2
+	Hammering Mizar by Learning Clause Guidance	2019	Jan Jakubův Josef Urban	2
+ PDF Chat	Matching Concepts across HOL Libraries	2014	Thibault Gauthier Cezary Kaliszyk	2
+ PDF Chat	The On-Line Encyclopedia of Integer Sequences	2007	N. J. A. Sloane	2
+ PDF Chat	A Proof Strategy Language and Proof Script Generation for Isabelle/HOL	2017	Yutaka Nagashima Ramana Kumar	2
+ PDF Chat	ATP and Presentation Service for Mizar Formalizations	2012	Josef Urban Piotr Rudnicki Geoff Sutcliffe	2
+ PDF Chat	ENIGMA-NG: Efficient Neural and Gradient-Boosted Inference Guidance for E	2019	Karel Chvalovský Jan Jakubův Martin Suda Josef Urban	2
+ PDF Chat	ENIGMA: Efficient Learning-Based Inference Guiding Machine	2017	Jan Jakubův Josef Urban	2
+ PDF Chat	CLS-SMT: Bringing Together Combinatory Logic Synthesis and Satisfiability Modulo Theories	2019	Fadil Kallat Tristan Schäfer Anna Vasileva	2
+	XGBoost	2016	Tianqi Chen Carlos Guestrin	2
+	Joint Training of Neural Network Ensembles.	2019	Andrew M. Webb Charles Reynolds Dan-Andrei Iliescu Henry W. J. Reeve Mikel Luján Gavin Brown	2
+ PDF Chat	The Common HOL Platform	2015	Mark Adams	2
+	Reinforcement Learning of Theorem Proving	2018	Cezary Kaliszyk Josef Urban Henryk Michalewski Mirek Olšák	2
+ PDF Chat	The Tactician	2020	Lasse Blaauwbroek Josef Urban Herman Geuvers	1
+ PDF Chat	TacticToe: Learning to Prove with Tactics	2020	Thibault Gauthier Cezary Kaliszyk Josef Urban Ramana Kumar Michael Norrish	1
+	Deep Symbolic Regression for Recurrent Sequences	2022	Stéphane d’Ascoli Pierre-Alexandre Kamienny Guillaume Lample François Charton	1
+	Hindsight Experience Replay	2017	Marcin Andrychowicz Filip Wolski Alex Ray Jonas Schneider Rachel H. Fong Peter Welinder Bob McGrew Joshua W.D. Tobin Pieter Abbeel Wojciech Zaremba	1
+	Number Theory: An Elementary Introduction Through Diophantine Problems	2010	Daniel Duverney	1
+	Structure Formation in Large Theories	2015	Serge Autexier Dieter Hutter	1
+	Über die Bausteine der mathematischen Logik	1924	M. Schönfinkel	1
+	Proof Pattern Search in Coq/SSReflect.	2014	Jónathan Heras Ekaterina Komendantskaya	1
+	BliStr: The Blind Strategymaker	2013	Josef Urban	1
+ PDF Chat	Effective Approaches to Attention-based Neural Machine Translation	2015	Thang Luong Hieu Pham Christopher D. Manning	1
+ PDF Chat	Structure Formation in Large Theories	2015	Serge Autexier Dieter Hutter	1
+ PDF Chat	Premise Selection for Mathematics by Corpus Analysis and Kernel Methods	2013	Jesse Alama Tom Heskes Daniel Kühlwein Evgeni Tsivtsivadze Josef Urban	1
+	Die Widerspruchsfreiheit der allgemeinen Mengenlehre	1937	Wilhelm Ackermann	1
+	The HOL Light Theory of Euclidean Space	2012	John Harrison	1
+	Nearest neighbor pattern classification	1967	Thomas M. Cover Peter E. Hart	1
+	Learning-assisted theorem proving with millions of lemmas	2014	Cezary Kaliszyk Josef Urban	1
+	Modular Elliptic Curves and Fermat's Last Theorem	1995	Andrew Wiles	1
+	Learning a SAT Solver from Single-Bit Supervision	2018	Daniel Selsam Matthew Lamm Benedikt Bünz Percy Liang Leonardo de Moura David L. Dill	1
+	First Experiments with Neural Translation of Informal to Formal Mathematics	2018	Qingxiang Wang Cezary Kaliszyk Josef Urban	1
+ PDF Chat	PaMpeR: proof method recommendation system for Isabelle/HOL	2018	Yutaka Nagashima Yilun He	1
+	Evolving Combinators	1997	Matthias Fuchs	1
+ PDF Chat	The On-Line Encyclopedia of Integer Sequences	2019	N. J. A. Sloane	1
+	SEPIA: Search for Proofs Using Inferred Automata	2015	Thomas Gransden Neil Walkinshaw Rajeev Raman	1
+ PDF Chat	Lemma Mining over HOL Light	2013	Cezary Kaliszyk Josef Urban	1
+	Internal Guidance for Satallax	2016	Michael Färber Chad E. Brown	1