Fwd: "Lean for the Curious Mathematician" at ICTS

[Siddhartha Gadgil]

Dear All,

       We are happy to announce that we are organizing "Lean for the Curious Mathematician" at ICTS from April 24 to April 26, 2025. Details are at https://www.icts.res.in/discussion-meeting/LCMaths. This will be an introduction to proving formally in the Lean Theorem Prover. 

       If you are interested in participating, please register by March 15, 2025 at the website https://www.icts.res.in/discussion-meeting/LCMaths.

Lean for the Curious Mathematician | ICTS Interactive Theorem Provers (or Proof Assistants) are tools that verify and partially automate mathematical proofs. The process of encoding mathematics into these systems, known as formalisation, has gained significant interest due to its role in proof verification, generating verified code for computer algebra systems, and expanding digital mathematical libraries. www.icts.res.in

With best regards,

Siddhartha Gadgil,

T.V.H. Prathamesh,

Ashvni Narayanan

[Siddhartha Gadgil]

---------- Forwarded message ---------
From: Siddhartha Gadgil <gad...@iisc.ac.in>
Date: Fri, 7 Mar 2025 at 13:35
Subject: Re: "Lean for the Curious Mathematician" at ICTS
To: ALL @ MATH <all....@iisc.ac.in>, Math Seminar Mailing List <maths...@iisc.ac.in>, Campus Bulletin <campusb...@iisc.ac.in>
Cc: prathame...@krea.edu.in <prathame...@krea.edu.in>, ashvni.n...@sydney.edu.au <ashvni.n...@sydney.edu.au>

Dear All,

       A reminder that registrations for "Lean for the Curious Mathematician" close in a week. Also, if you are a "senior" mathematician (for example a faculty member) and the form needs you to fill in a referee, please fill "Siddhartha Gadgil" (or the name of one of the other organizers). This is easier administratively than going through the invitation process.

regards,

Siddhartha

---

From: Siddhartha Gadgil
Sent: 26 February 2025 10:45
To: ALL @ MATH <all....@iisc.ac.in>; Math Seminar Mailing List <maths...@iisc.ac.in>; Campus Bulletin <campusb...@iisc.ac.in>
Cc: prathame...@krea.edu.in <prathame...@krea.edu.in>; ashvni.n...@sydney.edu.au <ashvni.n...@sydney.edu.au>
Subject: "Lean for the Curious Mathematician" at ICTS