I am the Director of the Artificial Intelligence and its Applications Institute (AIAI) (and previously that of the Centre for Intelligent Systems and their Applications), which is part of the School of Informatics at the university of Edinburgh.

I am also an Academic Lead and a member of the core management team for the University of Edinburgh’s new £20m Advanced Care Research Centre.

My main field of research lies in AI Modelling, which spans areas such as interactive theorem proving, formal verification, process modelling, and AI/machine learning applied to healthcare and other complex domains.

These days, I am particularly interested in the interactions between and combination of symbolic and data-driven approaches to Artificial Intelligence. More information about current research interests, projects etc. can be found on our AI Modelling Lab (AIML) website.


PhD in AI for Health and care: Are you interested in developing and applying AI techniques ranging from formal verification to machine learning to real-world health and care processes? Are you interested in Explainable AI for health and care? If the answer is yes to any of these questions, contact me. Funding may be available for good candidates.

PhD in Formal Modelling and Verification for AI: I am interested in supervising PhD students who wish to explore and develop the foundations of AI algorithms and approaches, e.g. machine learning (including Deep Learning) and logic-based learning, via formal modelling and verification. Candidates will need to have a strong  background in mathematics, an interest in computational logic/theorem proving and experience in machine learning and other aspects of AI. Funding is available for strong applicants.

PhD in Formalised Mathematics for Physics: I am looking for research students interested in  the  formalization of physics, whether theoretical or with a view towards its applications to the real world (e.g. the formal verification of safety properties related to robotics and autonomous navigation). Funding may be available for strong students.

PhD in Collaborative Theorem Proving: I am interested in supervising students on the application of machine learning and social computation to interactive theorem proving. Funding may be available for good students.

Some of my latest research interests:

  • AI for health and care, with an emphasis on the modelling of computer- and human-based processes and their interactions using AI techniques, and on the use of of AI/ML for predictive and causal modelling in health and care. More information is available on the AIML webpage.
  • Formal verification for AI/ML, especially with regards to reinforcement learning, autonomous agents and differentiable programs.
  • Formalised mathematics: I am working  on the formal reconstruction in the theorem prover Isabelle of proofs from Euler‘s famous Introductio in analysin infinitorum (Introduction to the Analysis of the Infinite), first published in 1748 and on Euler’s Institutiones calculi differentialis  (Foundations of differential calculus). More generally, I am interested in all aspects of formalised mathematics.
  • Process modelling for complex systems including manufacturing, healthcare and beyond.
  • I am currently working on various concepts related to the notion of Collaborative Mechanical Theorem Proving.

Latest Refereed Publications (kind of up-to-date):

  • Burton J, McMinn M., Vaughan J., Fleuriot J., Guthrie B. (2021). Care-home outbreaks of COVID-19 in Scotland March to May 2020: national linked data cohort analysis. Age and Ageing Journal, Volume 50, Issue 5, September 2021, 1482–1492, Oxford University Press.
  • Papapanagiotou P. and Fleuriot J. (2021). Object-level Reasoning with Logics Encoded in HOL Light. Electronic Proceedings in Theoretical Computer Science 332, pp. 18–34.
  • Fleuriot J. D. (2021). Mechanizing Mathematics: From Dream to Reality. Chapter in Mathematical Reasoning: The History and Impact of the DReaM Group (Ed. G. Michaelson), Springer.
  • Papapanagiotou P., Vaughan J., Smola F, and Fleuriot J. (2020). A Real-world Case Study of Process and Data Driven Predictive Analytics for Manufacturing Workflows. To appear in the proceedings of the 54th Hawaii International Conference on System Sciences (HICSS-54).
  • Wingfield L., Ceresa C., Thorogood S., Fleuriot J, Knight S. (2020). Artificial Intelligence and Liver Transplant: Predicting Survival of Individual Grafts, A Systematic Review. Liver Transplantation, Volume 26, Issue7, 922-934 .
  • Wingfield L., Ceresa C., Fleuriot J, Knight S. (2019). Artificial Intelligence for Liver Transplant (AI4T): Predicting Graft Survival. ASiT/TMS Poster of Distinction Prize. Association of Surgeons in Training International Surgical Conference 2019, British Journal of Surgery (BJS), Volume 106, Issue S6

 Recent Working Papers:

  • Chevallier M. and Fleuriot J.  (2021). Formalising the Foundations of Discrete Reinforcement Learning in Isabelle/HOL. arXiv:2112.05996.
  • Charlton C. E, Poon M. T. C., Brennan P. M. and Fleuriot J. D. (2021) Interpretable Machine Learning Classifiers for Brain Tumour Survival Prediction. arXiv:2106.0942.
  • Schmoetten R, Palmer J. E, Fleuriot J. D. (2021). Towards Formalising Schutz’ Axioms for Minkowski Spacetime in Isabelle/HOL. arXiv:2108.10868.
  • MacKenzie C, Fleuriot J. and Vaughan J. (2021). An Evaluation of the Archive of Formal Proofs. arXiv:2104.01052.
  • Scott P. and Fleuriot J. D. (2019). Where are the Natural Numbers in Hilbert’s Foundations of Geometry? arXiv:1911.07057.

A Few Papers currently in Preparation:

  • Machine Learning for Rare Diseases: a Glioblastoma Case Study.
  • Mechanizing the Hyperdual Numbers in Isabelle/HOL.
  • L’Hospital’s Theorems and Euler’s Notions of Orders of Infinity in Isabelle/HOL.
  • Mechanizing Minkowski Spacetime.
  • Reconstructing Euler in Isabelle: The Exponential Series as an Infinite Polynomial.
  • Formalising Meek’s Method of Single Transferable Vote.

Comments are closed.