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
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.
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.
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.
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.
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.
