Upcoming Events

The Kotak IISc AI-ML Centre welcomes you to an event on ‘Formalisation, Mathematics, and Artificial Intelligence’. This event will be a series of three talks on the closely-related areas of formalisation, mathematical reasoning, and artificial intelligence. 

Date: 21 April 2025 (Monday)
Time: 2:00–5:15 PM
Venue: Faculty Hall, IISc
Schedule:

  • 2:00–3:00 PM: Koundinya Vajjha (Formal Verification Engineer, Intel Corporation) will speak on ‘Formal Verification for Mathematics, Software, and Hardware’
  • 3:00–4:00 PM: Bhavik Mehta (Chapman Fellow in Mathematics, Imperial College, London) will speak on ‘Mathematics, AI, and Lean’
  • 4:00–4:15 PM: Coffee break
  • 4:15–5:15 PM: Patrick Massot (Professor, Université Paris-Saclay, Saint-Aubin, France) will speak on ‘Why Formalise Mathematics?’

Faculty organiser: Professor Siddhartha Gadgil, Department of Mathematics, IISc

A background: Formalisation is the verification of proofs by a computer. The proofs can be of mathematical results or of correctness of software, hardware, networking protocols, cryptographic systems, etc. 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 more wide adoption of formalisation is the relative difficulty of formalisation as compared to testing. With the development of artificial intelligence-based tools, this barrier can be considerably reduced.

On the other hand, while artificial intelligence (AI) 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, hardware, etc.