## About me

Since June 2024, I work as a Formal Verification Engineer at Apple.

Previously, I was a Computer Science PhD student at the University of Edinburgh, supervised by Dr Paul Jackson. I was part of the Laboratory for Foundations of Computer Science and the AI Modelling Lab. During my PhD, I worked on CvxLean, a verified convex optimization modeling framework written in Lean. The tool allows users to formulate optimization problems and rigorously transform them into equivalent solver-compatible forms in a semi-automatic fashion.

Before that, I obtained an MEng in Mathematics and Computer Science from Imperial College London (see my thesis) and a Logic Year certificate from the Institute for Logic, Language and Computation.

My main interests are interactive and automated theorem proving, and validated numerics.

E-mail:

GitHub | Google Scholar | dblp | LinkedIn

## Publications

##### Transforming optimization problems into disciplined convex programming form

*R. Fernández Mir, P. Jackson, S. Bhat, A. Goens, T. Grosser*

To appear in: Conference on Intelligent Computer Mathematics (**CICM**), 2024.

(PDF)

##### 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**), early access, pp.1-21, 2024.

(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 (**ExpMath**), Vol 31(2), pp.355-363, 2022.

(publisher's website | arXiv | GitHub)