ERC Consolidator Grant 2020: Assia Mahboubi - formalising the foundations of mathematics

Date:
Changed on 07/01/2021
Assia Mahboubi, a member of the Gallinette project team at the Inria Rennes - Bretagne Atlantique research centre, has just been awarded an ERC (European Research Council) Consolidator Grant for 2020.
Her field of expertise is type theory, the academic study of formal or “type” systems in mathematics, which involves the use of verification programs known as “proof assistants” to formalise mathematical results

Could you tell us about your research project at Inria?

My field of research is type theory, with a particular emphasis on its use for formalising foundations of mathematics. What I am interested in is the practical formalisation of mathematical results in the form of digital libraries using programs known as proof assistants. Proof assistants reduce theorem proof verification to a mechanical process performed by a single trusted program, which constitutes the core of the proof assistant.

But formalisation isn’t just about verification – it can also be used to “do” mathematics, whether it’s studying similarities between proofs, identifying new ones, revealing relevant abstractions, etc. However, one of the challenges when it comes to building these libraries is to bridge the gap between the language used to discuss mathematics in the literature or at seminars, and the much purer language used to mechanically verify whether or not a given statement is properly formed, or whether or not a proof is correct. Achieving this requires the use of a wide range of IT techniques, derived from programming language theory, but also from proof theory, automated theorem proving, etc.

Equipe-projet Gallinette

This year, you have been awarded an ERC grant. Which project did you receive this grant for?

I was awarded the grant for the FRESCO (Fast and Reliable Symbolic Computation) project, which aims to improve the reliability of the results produced by formal computational algorithms. Today, computers are essential to research in all fields of mathematics, even the most abstract. They are used to formulate conjectures and also to consolidate levels of proof. But verifying computational correction is often very difficult. We are striving to enable computational mathematics to benefit from the spectacular recent developments in formal methods, and especially the degree of maturity acquired by proof assistants.

 

What was your personal motivation for participating in this project?

Computer algebra systems and proof assistants are both used to represent and operate sophisticated mathematical objects on machines. However, these two types of tools are developed by entirely separate communities with different motivations: one is interested in efficiency, while the other is concerned with algebraic correction. I began to take an interest in the convergence of these two perspectives while studying for my PhD. But the contrast between the recent success of formal methods in fields such as security and compilation, and the almost total absence of formally verified tools for computational mathematics convinced me to start tackling this problem in earnest. Then, through various discussions with colleagues from a wide range of different scientific backgrounds (computer algebra, number theory, computer arithmetics, type theory, etc.), I was able to figure out the best strategy to adopt.

 

What does this grant mean for you?

First and foremost, it’s a huge opportunity and the start of an exciting adventure. Having this grant means we won’t have to worry about funding for our research for a quite some time, which is a real luxury, allowing us to focus on the scientific project itself. It’s also recognition on an academic level, and for that I feel indebted to my close colleagues who helped put the project together, especially Guillaume Melquiond, a researcher on the Toccata project team.

FRESCO also draws on the Coq proof assistant, which was first developed by Inria researchers more than 30 years ago. Without the developers’ creativity and their continued interactions with users, it would never have seen the light of day.

 

How do you intend to use the grant?

The funding will enable us to build a team of researchers that ticks all the boxes in terms of the scientific profiles required.

The team will then be able to pool its expertise in order to design and build a new working environment for computational mathematics. It's a real asset.

 

Are there any areas of research you would like to explore in the future?

It’s really too hard to say at the moment. A lot will depend on the progress made in the fields of research I’m interested in, but also - and, perhaps, most importantly - on the people I meet in a professional context.

Portrait d'Assia Mahboubi

 

Cinq dates clés dans le parcours d'Assia Mahboubi

  • 2006: Awarded a PhD in computer science from the University of Nice - Sophia Antipolis
  • 2006-2007: Research engineer at the Inria - Microsoft research centre
  • 2007: Recruited by Inria as a research fellow
  • 2017: Joined the Gallinette project team in Nantes
  • 2020: Awarded an ERC Consolidator Grant

 

 

To know more about it