Michael Rawson
e-mail webpage ORCID publication list Google Scholar Last updated .Timeline
- 2025–
- New Frontiers Fellow, University of Southampton, UK
- 2021–25
- Projektassistent, TU Wien, Austria
- 2020–21
- Research Associate, University of Manchester, UK
- 2017–21
- PhD, University of Manchester, UK
- 2014–17
- BA Computer Science, University of Cambridge, UK
Research Interests
I am most interested in the theory and practice of automated theorem proving for classical first-order logic, including machine-learned heuristic methods and proof reconstruction. I have also applied automated reasoning to security, protocol design, verification, and interactive theorem proving.
I develop the world-class automated theorem prover Vampire with an international team. Vampire has seen widespread use in many areas, particularly as automation for interactive systems. Increasingly it is also used standalone in research mathematics, notably algebra.
Awards
- 2025
- Learning to do Math with Vampires and Spiders funded via AI for Math.
- Distinguished paper The Vampire Diary at CAV.
- 2017–20
- Doctoral study funded by the School of Computer Science.
Organisation
Program Committees
Doctoral Examination
- Gonçalo Araújo
- NOVA Lisbon, 2025
Student Supervision
- Joe Hall
- Automated Finite Model Building for First-Order Logic (part III, 2025–26)
Teaching
- 2026
- Formal Specification and Verification — co-design and delivery of new undergraduate course, ca. 300 students. Nominated by student union for the Most Engaging Lecturer award.
- 2024
- Formal Methods Seminar, a small group reading research papers.
- Lecturer at the SAT/SMT/AR summer school.
- 2017–21
- Teaching assistant, various undergraduate and postgraduate courses.
- 2019
- Outreach lectures and activities for sixth form students.
- 2014–17
- STIMULUS volunteer in local schools.
- 2016
- Internship: designed second-year undergraduate computer graphics practical coursework.
Invited Talks
- 2025
- Automated Reasoning for the Working Mathematician. Workshop: AI Transforms Math Research, Augsburg
- 2023
- Deploying Neural Models for Theorem Proving. Joint EuroProofNet Workshops, Prague
- 2022
- Machine Learning for Theorem Proving: What I Wish I had Known 5 Years Ago. Conference on Artificial Intelligence and Theorem Proving, Aussois.
Research Visits
- 2026
- Saclay, France. Frédéric Blanqui, Formal Mathematics and Proof Systems Interoperability.
- 2022
- Scheidegg, Germany. Wolfgang Bibel, Christoph Wernhard, Zsolt Zombori. Use of lemmata in connection systems.
- 2019
- CIIRC Prague, Martin Suda and Josef Urban. Learning-guided automated theorem proving.