Department of Computer Science and Technology,
University of Cambridge,
William Gates Building,
15 JJ Thomson Avenue,
Cambridge CB3 0FD, UK
I am a research associate at University of Cambridge, working with Prof. Larry Paulson. My research interest includes
- machine learning for theorem proving,
- interactive theorem proving,
- verified symbolic computing,
- and mechanised mathematics.
I believe modern machine learning techniques will revolutionise the way people do mechanised proofs, so that we can build more reliable systems.
I will be joining the University of Edinburgh as a lecturer (equivalent to assistant professor in the US) in September. I will have full scholarships for home and international students - if you want to pursue a PhD with me, please get in touch.
- arXivDecomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Proving2023
- ICLR (oral)Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal ProofsIn The Eleventh International Conference on Learning Representations 2023
- NeurIPSThor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers2022
- ICMLLime: Learning inductive bias for primitives of mathematical reasoningIn International Conference on Machine Learning, 2021
- ICLRIsarStep: a Benchmark for High-level Mathematical ReasoningIn International Conference on Learning Representations, 2021
- JAREvaluating winding numbers and counting complex roots through Cauchy indices in Isabelle/HOLJournal of Automated Reasoning 2020
- JARDeciding univariate polynomial problems using untrusted certificates in Isabelle/HOLJournal of Automated Reasoning, 2019