Overview: In this workshop, we will provide an introduction to the fundamentals of theorem proving and the incorporation of Large Language Models (LLMs) within this field. Starting with a brief history on theorem proving and its applications, we will proceed to discuss the basics of the Lean theorem-proving language and walk through some simple examples. Next, we will discuss how some machine learning tools, particularly LLMs, have been applied in theorem proving and the tools available to mathematicians for research or education. Finally, we will briefly address the current limitations, potentials, and future research directions in the field of theorem proving and mathematical reasoning with LLMs.

Prerequisites:
- Basic familiarity with at least one programming language, e.g., Python.

Location: HYBRID. Online via Zoom, or in-person at Burnside Hall room 1104 (11th floor).
Instructor: Mohammad Pedramfar, Postdoctoral Researcher at Mila/McGill

IMPORTANT NOTE: for those attending the workshop online, you must log-into your McGill Zoom account. Otherwise, the link will not work. You can do so on the browser here: https://mcgill.zoom.us/ . For more information on McGill Zoom, please visit this website: https://www.mcgill.ca/tls/students/learning-resources/use-technology/learning-zoom