Mini-Course: An Introduction to Automatic Theorem-Proving in Mathematics

Mini-Course: An Introduction to Automatic Theorem-Proving in Mathematics

Time:

Venue/Location: Vietnam Institute for Advanced Study in Mathematics (VIASM), 161 Huynh Thuc Khang Street, Hanoi

Objective: Over the last few years, formal proof assistants - together with the new generation of AI copilots - have moved from a niche curiosity to a  tool that working mathematicians can no longer afford to ignore.

This mini-course offers a hands-on introduction to this rapidly developing area, aimed at mathematicians and advanced students with no prior experience in formalization. We begin with a gentle exposition of the type-theoretic foundations  underlying modern proof assistants, focusing on the conceptual picture rather than the technicalities. We then survey the major formalization  systems in use today (Lean, Coq/Rocq, Isabelle, Agda) and discuss why Lean and its mathematical library Mathlib have become a natural meeting point for the mathematical community.

The heart of the course is practical. We will run a workshop in which all participants install Lean and, working together - by hand and with the help of AI assistants such as Claude, Codex, Aristotle, and Gauss  - formalize a concrete theorem from scratch. Through this example we will discuss the choice of definitions, common pitfalls, and small tricks that make formalization tractable. From there we move to a deeper look at Lean's tactic language, and we close with a discussion of how to design a good formalization project: choosing a target, decomposing it into manageable pieces, and collaborating effectively  with both human contributors and AI tools. By the end of the course, participants should have a working Lean installation, a feel for the day-to-day rhythm of AI-assisted formal proof, and a clear sense of how to begin a formalization project of their own.

Lecturer

  • Bartosz NaskrÄ™cki, Adam Mickiewicz University, Poland.

Program Committee

  • Dao Hai Long, University of Kansas, USA;
  • Le Minh Ha, Vietnam Institute for Advanced Study in Mathematics (VIASM).

Expected participants: Lecturers, students, and scientists who are genuinely interested in using automated proof and formalization in scientific research. A certain level of expertise is required, and preference will be given to those who already have ideas for experimentation, however small.

Organizers & Sponsors:

  • Vietnam Institute for Advanced Study in Mathematics (VIASM);
  • Vietnam Innovation of Education Foundation (VIEF).

Format: In person

Language: English

Registration: HERE

Registration is free but compulsory. 

Deadline: July 20, 2026

Contact: Ms. Tran Thuy Linh (VIASM), ttlinh@viasm.edu.vn