Formalisation, Mathematics, & Artificial Intelligence

Date: 21 April 2025

Formalisation is the verification of proofs by a computer. The proofs can be of mathematical results or of correctness of software, hardware, networking protocols, and cryptographic systems. Formalisation is often done with interactive theorem provers (such as the Lean prover), which help in finding proofs in addition to ensuring correctness. The use of formalisation has grown greatly in industry, as increasingly complex and critical systems testing is not adequate to guarantee correctness, hence security and safety. The main barrier to a wider adoption of formalisation is the relative difficulty of formalisation as compared to testing. With the development of artificial intelligence (AI)-based tools, this barrier can be considerably reduced.

On the other hand, while artificial intelligence systems have become very powerful, they still have issues with accuracy. In many domains (including mathematics), as errors cascade, even a relatively small rate of incorrect responses acts as a barrier to scaling and autonomy. It is widely believed that the best solution to this is to use formalisation (also assisted by AI) to ensure correctness and enable scalability and autonomy. Thus, formalisation and artificial intelligence promise to work together to allow computers to greatly assist mathematical reasoning as well as the development of software and hardware.

A series of three talks on the closely related areas of formalisation, mathematical reasoning, and artificial intelligence was organised by the Kotak IISc AI-ML Centre (KIAC) on 21 April 2025. The programme was structured and hosted by Siddhartha Gadgil (Professor, Department of Mathematics, IISc). The talks were by three eminent mathematicians, namely, Koundinya Vajjha (Formal Verification Engineer, Intel Corporation), Bhavik Mehta (Chapman Fellow in Mathematics, Imperial College, London), and Patrick Massot (Professor, Université Paris-Saclay, Saint-Aubin, France). Together, they gave the audience an introduction to formalisation – its use in mathematics, software, and hardware, and limitations; how AI has been able to do mathematics; and the working of the Lean prover.