About me
Since May 2026, I work as a Research Engineer at Harmonic. My work centers on combining interactive theorem proving (Lean) and agentic AI (Aristotle) to tackle large-scale verification problems.
Previously, I worked as a Formal Verification Engineer at Apple, focusing on numerical hardware.
Before that, I was a PhD student at the University of Edinburgh, supervised by Dr Paul Jackson. During my PhD, I contributed to CvxLean, a verified convex optimization modeling framework.
Popping from the stack once again, I studied Mathematics and Computer Science at Imperial College London and Logic at the ILLC in Amsterdam.
I'm broadly interested in formal methods, and their applications to hardware verification. Always happy to talk about these topics!
E-mail:
GitHub | Google Scholar | dblp | LinkedIn
Theses
Verified transformations for convex programming
PhD thesis, University of Edinburgh, 2024
(PDF)
Schemes in Lean
MEng thesis, Imperial College London, 2019
(PDF)
Publications
Transforming optimization problems into Disciplined Convex Programming form
R. Fernández Mir, P. B. Jackson, S. Bhat, A. Goens, T. Grosser
International Conference on Intelligent Computer Mathematics (CICM), Vol 14960, pp.183-202, 2024.
(publisher's website)
Verified reductions for optimization
A. Bentkamp, R. Fernández Mir, J. Avigad
International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), Vol 13994, pp.74-92, 2023.
(publisher's website | arXiv | GitHub)
Machine-learned premise selection for Lean
B. Piotrowski, R. Fernández Mir, E. Ayers
International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), Vol 14278, pp.175-186, 2023.
(publisher's website | arXiv | GitHub)
Conference on Artificial Intelligence and Theorem Proving (AITP), 2023.
(extended abstract)
Neurosymbolic AI for reasoning over knowledge graphs: a survey
L. N. DeLong, R. Fernández Mir, J. D. Fleuriot
IEEE Transactions on Neural Networks and Learning Systems (IEEE TNNLS), Vol 36(5), pp.7822-7842, 2025.
(publisher's website | GitHub)
Schemes in Lean
K. Buzzard, C. Hughes, K. Lau, A. Livingston, R. Fernández Mir, S. Morrison
Journal of Experimental Mathematics (Exp Math), Vol 31(2), pp.355-363, 2022.
(publisher's website | arXiv | GitHub)