Language models have shown remarkable abilities: processing natural language, analogical reasoning, even generating mathematical proofs. However, the arguments they generate often have logical flaws, and they are poor at judging correctness. It is thus natural to hope that pairing them with a formal proof system like Lean will be useful.
In this talk we first discuss using Large Language Models (LLMs) to generate Lean code from natural language statements. We then discuss extending this to more complex tasks using intertwined informal and formal mathematics using LLMs and the Lean prover. The latter part will be informal and will consist for the most part of examples of uses of language models and their limitations.
—-
WATCH ONLINE HERE : https://www.microsoft.com/en-gb/microsoft-teams/join-a-meeting?rtc=1 Meeting ID: 370 771 279 261 Passcode: iCo7a5
