AIMAG: FUNDAMENTALS OF LEAN

An open group of mathematicians to learn formalization, explore artificial intelligence, and develop research projects.

By mathematicians for mathematicians

Course Overview

Eight 90-minute sessions to write and understand formal proofs, starting from familiar mathematics.

  • Dates: January 13 – March 3, 2027
  • Schedule: Wednesdays · 12:15–13:45
  • Format: IMAG (Granada) + Online
  • Prerequisites: Master’s degree level in mathematics. Lean and programming taught from scratch.
  • Target Audience: Open to participants from any university or research center.

The Program

  1. Session 01 | Reading a proof (Jan 13)
    Recognize hypotheses, goals, and steps in a proof.
  2. Session 02 | Logic and cases (Jan 20)
    Translate implications and organize arguments by cases.
  3. Session 03 | Quantifiers (Jan 27)
    Work with “for all”, “there exists”, and witnesses.
  4. Session 04 | Equality and computation (Feb 3)
    Rewrite equalities and build chains of computation.
  5. Session 05 | Sets (Feb 10)
    Prove inclusions and equalities between sets.
  6. Session 06 | Functions and lemmas (Feb 17)
    Study functions and reuse previously proven results.
  7. Session 07 | Induction (Feb 24)
    Connect inductive arguments with formal proofs.
  8. Session 08 | A complete example (Mar 3)
    Go through a full formalization using the tools from the course.

Beyond the Course: Working Groups

A course as a starting point. After the course, we keep working. The AIMAG team will continue with formalization projects.
Working groups will be able to study a topic, develop their own examples, and present their progress at the seminar.

First Group · Geometry – Alexandrov’s Reflection Method

A geometric idea with applications in geometry and partial differential equations. Starting point: study its arguments and move forward,
lemma by lemma, toward its formalization. Shift the plane, reflect, and compare.


Alexandrov Reflection Method Diagram

Next Call: New Working Group Proposals

We will soon open the call for working group proposals, both from the University of Granada (UGR) and from other universities.
The idea: a professor coordinates a group of students around a mathematical topic. The groups will be presented on this website
and will share their progress with AIMAG.

Contact & Access: Access links for online sessions will be published prior to the start.
For inquiries about the course and participating in AIMAG, contact us at: leanimag@ugr.es

Visit the official website.