CAS Alumnus granted 34.7 million Swedish Kronor for analysing proofs

‘My project is about the analysis of proofs, mostly in mathematics,’ Thierry Coquand, a Professor of Computer Science at the University ofGothenburg, says.

Coquand receives 34.7 million Swedish Kronor from the Swedish Knut and Alice Wallenberg Foundation for his five-year project, which allows for time for research and help for funding PhD students and postdocs. 

How can we be sure that an argument is correct?

‘We will be designing so-called “proof assistants”, which are special programs that help to build a correct proof,’ Coquand says.  

The former CAS scholar says that the current main use of proof assistants is for checking complex software, for instance compilers when translating codes written in one programming language into another.

‘But the hope is that such systems will also be useful for mathematicians to explore complex and conceptually deep ideas, while ensuring that the arguments are always correct’.

In 2018/19, the French scholar was a fellow at the CAS project Homotopy Type Theory and Univalent Foundations led by Marc Bezem and Bjørn Ian Dundas. Coquand stayed at CAS for four months.

‘The stay at CAS indeed contributed to my work. It was really nice to have complete freedom and time to concentrate on my research’, Coquand says.  

He especially appreciated what he describes as “perfect interactions” with participants in the project who came from other fields than him.

‘I had some really nice exchanges of ideas with a philosopher of mathematics, Steve Awodey from the Carnegie Mellon University, and mathematician Emily Riehl from the John Hopkins University, starting projects that I am still working on.’

Knut and Alice Wallenberg Foundation granted financial support to 18 projects in total.

The foundation supports outstanding projects within fundamental research in medicine, the natural sciences and technology that have the potential for future scientific breakthroughs.