Learning to Reason with HOL4 tactics T Gauthier, C Kaliszyk, J Urban arXiv preprint arXiv:1804.00595, 2018 | 96* | 2018 |

Premise selection and external provers for HOL4 T Gauthier, C Kaliszyk Proceedings of the 2015 Conference on Certified Programs and Proofs, 49-57, 2015 | 45 | 2015 |

Matching concepts across HOL libraries T Gauthier, C Kaliszyk International Conference on Intelligent Computer Mathematics, 267-281, 2014 | 39 | 2014 |

Classification of alignments between concepts of formal mathematical systems D Müller, T Gauthier, C Kaliszyk, M Kohlhase, F Rabe International Conference on Intelligent Computer Mathematics, 83-98, 2017 | 27 | 2017 |

Sharing HOL4 and HOL Light proof knowledge T Gauthier, C Kaliszyk Logic for Programming, Artificial Intelligence, and Reasoning, 372-386, 2015 | 25 | 2015 |

Initial Experiments with Statistical Conjecturing over Large Formal Corpora. T Gauthier, C Kaliszyk, J Urban FM4M/MathUI/ThEdu/DP/WIP@ CIKM, 219-228, 2016 | 23 | 2016 |

TacticToe: learning to prove with tactics T Gauthier, C Kaliszyk, J Urban, R Kumar, M Norrish Journal of Automated Reasoning 65 (2), 257-286, 2021 | 21 | 2021 |

GRUNGE: A grand unified ATP challenge CE Brown, T Gauthier, C Kaliszyk, G Sutcliffe, J Urban International Conference on Automated Deduction, 123-141, 2019 | 15 | 2019 |

Aligning concepts across proof assistant libraries T Gauthier, C Kaliszyk Journal of Symbolic Computation 90, 89-123, 2019 | 15 | 2019 |

Deep reinforcement learning for synthesizing functions in higher-order logic T Gauthier arXiv preprint arXiv:1910.11797, 2019 | 10 | 2019 |

Deep reinforcement learning in HOL4 T Gauthier | 6 | 2019 |

Tree neural networks in HOL4 T Gauthier International Conference on Intelligent Computer Mathematics, 278-283, 2020 | 5 | 2020 |

Self-learned formula synthesis in set theory CE Brown, T Gauthier arXiv preprint arXiv:1912.01525, 2019 | 5 | 2019 |

Beagle as a HOL4 external ATP method T Gauthier, C Kaliszyk, C Keller, M Norrish PAAR-Fourth Workshop on Practical Aspects of Automated Reasoning, 2014 | 4 | 2014 |

Program Synthesis for the OEIS T Gauthier arXiv preprint arXiv:2202.11908, 2022 | 1 | 2022 |

Synthesis of Recursive Functions from Sequences of Natural Numbers1 T Gauthier | 1 | 2021 |

First experiments with data driven conjecturing K Chvalovskı, T Gauthier, J Urban | 1 | 2019 |

Conjecturing over large corpora T Gauthier, C Kaliszyk, J Urban, J Vyskocil Proceedings from the first conference on artificial intelligence and theorem …, 2016 | 1 | 2016 |

Proofgold: Blockchain for Formal Methods CE Brown, C Kaliszyk, T Gauthier, J Urban 4th International Workshop on Formal Methods for Blockchains (FMBC 2022), 2022 | | 2022 |

Learned Provability Likelihood for Tactical Search T Gauthier arXiv preprint arXiv:2109.03234, 2021 | | 2021 |