My personal interest in problem-solving is reflected in my research interests. I like to solve real-world problems through mathematics, and I love the way mathematics helps us understand reality. In the last decade, Machine Learning has proven itself as a very powerful tool to find solutions and improve people's lives, however, contrary to mathematics 

I am also interested in tools for checking the validity of mathematical proofs, this is why doing a PhD project on how to improve quantifier elimination procedures using machine learning was ideal for me.

Under the supervision of Matthew England, Kamal Bentahar and Vasile Palade my PhD project consists in using heuristics and machine learning to speed up these algebraic processes without affecting the mathematical validity of the results.

Many algebraic algorithms are proving themselves very useful in applied mathematics, for example, Cylindrical Algebraic Decomposition (CAD), non-uniformal Cylindrical Algebraic Decomposition (nuCAD) or Cylindrical Algebraic Covering (CAC). However, they have a huge complexity (double exponential w.r.t. the number of variables) and therefore some interesting problems can't be solved in a reasonable time.

In these algebraic algorithms, some choices must be taken, such as a variable ordering, a polynomial ordering or whether it's worth it to use some extra information that might take some time to compute. These choices affect immensely the resources needed to solve a problem without affecting the mathematical validity of the results. This sets the perfect scenario to involve Machine Learning to boost these algebraic procedures.