{"id":14699,"date":"2026-10-27T09:48:37","date_gmt":"2026-10-27T08:48:37","guid":{"rendered":"https:\/\/wpd.ugr.es\/~imag\/?page_id=14699"},"modified":"2026-10-27T10:14:41","modified_gmt":"2026-10-27T09:14:41","slug":"aimag-fundamentals-of-lean","status":"publish","type":"page","link":"https:\/\/wpd.ugr.es\/~imag\/aimag-fundamentals-of-lean\/","title":{"rendered":"AIMAG: FUNDAMENTALS OF LEAN"},"content":{"rendered":"<p><a href=\"https:\/\/wpd.ugr.es\/~imag\/cms\/wp-content\/uploads\/Captura-de-pantalla-2026-10-27-094518.png\"><img loading=\"lazy\" decoding=\"async\" src=\"https:\/\/wpd.ugr.es\/~imag\/cms\/wp-content\/uploads\/Captura-de-pantalla-2026-10-27-094518.png\" alt=\"\" width=\"300\" height=\"122\" class=\"aligncenter size-medium wp-image-14702\" srcset=\"https:\/\/wpd.ugr.es\/~imag\/cms\/wp-content\/uploads\/Captura-de-pantalla-2026-10-27-094518.png 481w, https:\/\/wpd.ugr.es\/~imag\/cms\/wp-content\/uploads\/Captura-de-pantalla-2026-10-27-094518-300x122.png 300w, https:\/\/wpd.ugr.es\/~imag\/cms\/wp-content\/uploads\/Captura-de-pantalla-2026-10-27-094518-465x189.png 465w\" sizes=\"(max-width: 300px) 100vw, 300px\" \/><\/a><\/p>\n<h1>AIMAG: FUNDAMENTALS OF LEAN<\/h1>\n<p>An open group of mathematicians to learn formalization, explore artificial intelligence, and develop research projects.<\/p>\n<p><strong>By mathematicians for mathematicians<\/strong><\/p>\n<h2>Course Overview<\/h2>\n<p>Eight 90-minute sessions to write and understand formal proofs, starting from familiar mathematics.<\/p>\n<ul>\n<li><strong>Dates:<\/strong> January 13 \u2013 March 3, 2027<\/li>\n<li><strong>Schedule:<\/strong> Wednesdays \u00b7 12:15\u201313:45<\/li>\n<li><strong>Format:<\/strong> IMAG (Granada) + Online<\/li>\n<li><strong>Prerequisites:<\/strong> Master&#8217;s degree level in mathematics. Lean and programming taught from scratch.<\/li>\n<li><strong>Target Audience:<\/strong> Open to participants from any university or research center.<\/li>\n<\/ul>\n<h2>The Program<\/h2>\n<ol>\n<li>\n    <strong>Session 01 | Reading a proof (Jan 13)<\/strong><br \/>\n    Recognize hypotheses, goals, and steps in a proof.\n  <\/li>\n<li>\n    <strong>Session 02 | Logic and cases (Jan 20)<\/strong><br \/>\n    Translate implications and organize arguments by cases.\n  <\/li>\n<li>\n    <strong>Session 03 | Quantifiers (Jan 27)<\/strong><br \/>\n    Work with &#8220;for all&#8221;, &#8220;there exists&#8221;, and witnesses.\n  <\/li>\n<li>\n    <strong>Session 04 | Equality and computation (Feb 3)<\/strong><br \/>\n    Rewrite equalities and build chains of computation.\n  <\/li>\n<li>\n    <strong>Session 05 | Sets (Feb 10)<\/strong><br \/>\n    Prove inclusions and equalities between sets.\n  <\/li>\n<li>\n    <strong>Session 06 | Functions and lemmas (Feb 17)<\/strong><br \/>\n    Study functions and reuse previously proven results.\n  <\/li>\n<li>\n    <strong>Session 07 | Induction (Feb 24)<\/strong><br \/>\n    Connect inductive arguments with formal proofs.\n  <\/li>\n<li>\n    <strong>Session 08 | A complete example (Mar 3)<\/strong><br \/>\n    Go through a full formalization using the tools from the course.\n  <\/li>\n<\/ol>\n<h2>Beyond the Course: Working Groups<\/h2>\n<p>\n  A course as a starting point. After the course, we keep working. The AIMAG team will continue with formalization projects.<br \/>\nWorking groups will be able to study a topic, develop their own examples, and present their progress at the seminar.\n<\/p>\n<h3>First Group \u00b7 Geometry &#8211; Alexandrov&#8217;s Reflection Method<\/h3>\n<p>\n  A geometric idea with applications in geometry and partial differential equations. Starting point: study its arguments and move forward,<br \/>\nlemma by lemma, toward its formalization. <em>Shift the plane, reflect, and compare.<\/em>\n<\/p>\n<p>\n  <a href=\"https:\/\/wpd.ugr.es\/~imag\/cms\/wp-content\/uploads\/Captura-de-pantalla-2026-10-27-094430.png\"><br \/>\n    <img loading=\"lazy\" decoding=\"async\"\n      src=\"https:\/\/wpd.ugr.es\/~imag\/cms\/wp-content\/uploads\/Captura-de-pantalla-2026-10-27-094430.png\"\n      alt=\"Alexandrov Reflection Method Diagram\"\n      width=\"500\"\n      height=\"300\"\n      class=\"aligncenter size-medium wp-image-14700\"\n    \/><br \/>\n  <\/a>\n<\/p>\n<h3>Next Call: New Working Group Proposals<\/h3>\n<p>\n  We will soon open the call for working group proposals, both from the University of Granada (UGR) and from other universities.<br \/>\nThe idea: a professor coordinates a group of students around a mathematical topic. The groups will be presented on this website<br \/>\nand will share their progress with AIMAG.\n<\/p>\n<p>\n  <strong>Contact &#038; Access:<\/strong> Access links for online sessions will be published prior to the start.<br \/>\nFor inquiries about the course and participating in AIMAG, contact us at:  <a href=\"mailto:leanimag@ugr.es\">leanimag@ugr.es<\/a><\/p>\n<p>Visit the <a href=\"https:\/\/imag.ugr.es\/AIMAG\/index.html\">official website<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>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 \u2013 March 3, 2027 Schedule: Wednesdays \u00b7 12:15\u201313:45 Format:<span class=\"more-link\"><a href=\"https:\/\/wpd.ugr.es\/~imag\/aimag-fundamentals-of-lean\/\">Continue Reading<\/a><\/span><\/p>\n","protected":false},"author":4,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"translation":{"provider":"WPGlobus","version":"3.0.0","language":"en","enabled_languages":["en"],"languages":{"en":{"title":true,"content":true,"excerpt":false}}},"_links":{"self":[{"href":"https:\/\/wpd.ugr.es\/~imag\/wp-json\/wp\/v2\/pages\/14699"}],"collection":[{"href":"https:\/\/wpd.ugr.es\/~imag\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/wpd.ugr.es\/~imag\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/wpd.ugr.es\/~imag\/wp-json\/wp\/v2\/users\/4"}],"replies":[{"embeddable":true,"href":"https:\/\/wpd.ugr.es\/~imag\/wp-json\/wp\/v2\/comments?post=14699"}],"version-history":[{"count":10,"href":"https:\/\/wpd.ugr.es\/~imag\/wp-json\/wp\/v2\/pages\/14699\/revisions"}],"predecessor-version":[{"id":14718,"href":"https:\/\/wpd.ugr.es\/~imag\/wp-json\/wp\/v2\/pages\/14699\/revisions\/14718"}],"wp:attachment":[{"href":"https:\/\/wpd.ugr.es\/~imag\/wp-json\/wp\/v2\/media?parent=14699"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}