A tool for autoformalization of mathematics in Lean
Speaker: Ashvni Narayanan (Imperial College, London)
| Speaker |
Speaker: Ashvni Narayanan (Imperial College, London)
|
|---|---|
| When |
Sep 12, 2023
from 02:00 PM to 03:00 PM |
| Where | Ground Floor Auditorium (006) |
| Add event to calendar |
vCal
iCal
|
Abstract : Formalization is the process of making a computer understand mathematics. It can often be difficult if one is not familiar with the nuances of the language. Automation attempts to make it easier for mathematicians to verify their results. We discuss a tool which has been created to aid autoformalization in a theorem prover called Lean. This is a joint work with Prof Siddhartha Gadgil, Dr Anand Tadipatri, Dr Navin Goyal and Ayush Agarwal.