Mathematician and professor of computer science at the University of Gothenburg, Sweden, Thierry Coquand is a proponent of constructivist philosophy in mathematics. He introduced the notion of construct calculus, on which proof assistant software such as Coq and Lean are based, enabling mathematical proofs to be represented and verified on the computer.
He has been invited to occupythe Computer Sciences and Digital Technologies chair, created in partnership with Inria, for the year 2024-2025 .
A nemesis for some students and a revelation for others, mathematics fascinates as much as it can seem impenetrable. Yet every piece of mathematical reasoning, however complex, can be broken down into simpler parts that help us to understand it. It's this observation, and the mysterious aura that shrouds this scientific discipline, that has captured the interest of Thierry Coquand, today a mathematician and professor of computer science at the University of Gothenburg in Sweden, ever since his junior high school days. What fascinates me is understanding what happens when you prove something," he explains. In mathematics, certain proofs, known as non-constructive proofs, seem magical in that they show the existence of an element without actually constructing it, but when you witness a magic trick, you want to understand the underlying trick, and that's what motivates, I think, constructivist mathematicians. "
Classically, and since thinkers like Aristotle and Plato, mathematics has been defined as a form of absolute and universal truth, prior to and external to its perception by man. But not all mathematicians agree on this definition, and some believe that mathematics, like language, is a product of the human mind. Constructivist philosophy takes this approach, stipulating that the existence of an object can only be demonstrated if we can establish a mental construction of it, i.e., a sequence of operations that effectively exhibits it. At the beginning of the 20th century, this philosophy was the subject of much debate, among renowned mathematicians such as David Hilbert, L.E.J. Brouwer and Henri Poincaré. One of the points raised was the problem of the axiom of choice and the principle of the excluded third, which allow for such non-effective proofs of existence. According to this principle, either a proposition is true, or its negation is true, and there is no third option. In sum : A is true or false ; Aristotle is alive or dead, for example. For L.E.J. Brouwer, this principle is not systematically verified in mathematics, and involves non-intuitive notions. However, constructivists aspire to a mathematical science that reconnects with intuition, and whose demonstrations are rooted in such palpable logic." For me, mathematics that dispenses with the excluded third is much more elegant, but not everyone agrees ", explains Thierry Coquand, who has worked mainly in algebra and, with Henri Lombardi and Claude Quitté, has succeeded in explaining several non-effective proofs of the existence of concrete objects in this field." We try to understand where such objects are in a mathematical proof, and every time we try to determine this, we feel we understand the proof itself better. "
Between mathematics and computer science
In the years 1980s, the work of certain computer scientists and problems of mathematical logic came very close together. What we now call functional programming was in full development," explains Thierry Coquand. And it was based on lambda-calculus, a theoretical programming language invented in the 1930s by the American logician Alonzo Church. " At the time, Dutch mathematician Nicolaas de Bruijn was trying to understand how to represent mathematics on a computer, in particular by developing a system capable of verifying proofs. He developed a formalism - a system of language and semantics designed to represent an object of study unambiguously - called type-dependent . Based on the lambda-calculus, this formalism has strong connections with constructive mathematics and is very similar to the formalism studied in parallel by logicians such as the Frenchman Jean-Yves Girard. A former student at the École normale supérieure, Thierry Coquand arrived in this context and worked on his thesis in 1985 to draw up a synthesis of these different kinds of lambda-calculus." As there was a connection with functional programming, I wanted to develop a unifying formalism that could be used both to establish mathematical proofs and to write programs ", he recalls. He carried out this work under the supervision of Gérard Huet, a specialist in functional programming and machine proofs, and introduced with him the notion of construct calculus.
This new formalism was still a little too formal at the time, and didn't seem to have any clear semantics, but it attracted the attention of a great Russian-American mathematician, Vladimir Voevodsky, who was also looking to represent mathematics on computers. As Voevodsky scoured the systems in which mathematical proofs are represented, he came across this formalism of dependent types and became fascinated by it. On closer examination, he realized that the formalism did indeed have a natural semantics, stemming precisely from his field of work : homotopy theory, the abstract study of forms in mathematics. Vladimir Voevodsky began to establish proofs in this formalism, in order to verify its suitability for representing mathematical notions in a satisfactory manner. As part of this effort, he organized a research year devoted to this problem at Princeton's Institute for Advanced Study in 2012-2013." This experiment attracted many young researchers in mathematics and computer science ", notes Thierry Coquand, who went to Princeton to coordinate the project with his Russian-American colleague." It gave rise to a very lively and exciting dialogue aimed at understanding the relationship between, on the one hand, this formalism that was trying to represent machine proofs and, on the other, homotopy theory. Research on the subject has now been going on for over ten years, thanks to young researchers who manage to reason directly within this framework of thought, in a way that was unthinkable just twenty years ago. I don't know where this will lead us, but it's very interesting and highlights this strong connection that exists between these different mathematical fields. "
Software to verify proofs
Another result of the formalism established by Thierry Coquand is the development of software called " Coq ", by a team at Inria and, more recently, Lean software developed in the USA. It is a proof assistant whose logic is based on the calculus of constructs, and whose aim is to help mathematicians and computer scientists verify mathematical proofs. The principle is simple : the user interacts with the system by formulating a mathematical statement and its proof, then the system checks that the statement is correctly formulated, and then verifies the correctness of this proof. This is a valuable tool for researchers who want to prove systems or programs such as compilers. It is also useful in the theory of programming languages, for fine-tuning these languages and showing that they are based on the right properties.
In mathematics, proofs often take longer and longer, and some mathematicians have realized that results are sometimes so complicated that nobody really checks them. Vladimir Voevodsky had presented one of his results in a lecture several times, then, during a new, more detailed lecture, he noticed that both the proof he was giving and the result he had derived from it were wrong, even though it had already been quoted and used by other mathematicians. This led him to realize that other results in his field, long thought to be correct, were not. And yet, in mathematics, some people tackle open problems by basing their thoughts and work on previously established results. This is sometimes a long process, spread over several years." Then, when the proof used as a foundation turns out to be false after detailed examination, it's really terrible," laments Thierry Coquand. " This problem of trust has made it difficult for many people to collaborate, as the results cannot be used with the same degree of absolute certainty as, say, black boxes. Fortunately, thanks to proof assistants such as Coq or Lean software, collaborative work between mathematicians will once again be able to flourish. We can launch problems that can be studied by dozens of people around the world," enthuses Thierry Coquand. And we can be sure of their correctness, because their results will be checked by the correction assistant. That's what's happening more and more. " Ideally, and in the long term, these software programs should be able to do even more than this ; in particular, by helping researchers to find proofs, in addition to verifying them.
The challenges of mathematics
One of the major difficulties encountered by Thierry Coquand in establishing his formalism was representing a notion that is nonetheless elementary in mathematics : equality. This difficulty kept him on his toes for almost thirty years. While this formalism did manage to represent fairly concrete mathematics, such as the theory of graphs or finite groups, it failed to represent his more abstract leanings, such as analysis or category theory. It was working with Vladimir Voevodsky, from a different mathematical field, that finally broke the deadlock. Thanks to our dialogue, I realized that you need to know things like homotopy theory to understand equality in this formalism," says Thierry Coquand. This shows that it takes a real capacity for transversality to overcome problems, and to open up to other areas of mathematics in which we ourselves are not specialists. It leads me to learn something new and totally captivating. "
For the year 2024-2025, Thierry Coquand holds the Computer Sciences and Digital Technologies Annual Chair at the Collège de France, an appointment he receives with great humility and interest. It's an opportunity for him to reflect on what's important to address in his discipline, which is sometimes difficult to represent to a wide audience." I feel responsible, in a way, for the field of constructivist mathematics, on the occasion of these lectures, but I'm looking forward to presenting the ins and outs of the field, and the problems that remain to be solved ! " An opportunity, perhaps, to inspire potential young researchers as he already did ten years earlier during the special year organized at Princeton's Institute for Advanced Study.
Article by William Rowe-Pirra
