Latest News
Workshop on LEAN
The Department of Mathematics is organizing an introductory workshop on the Lean proof assistant from 26th to 28th February. The workshop will introduce the participants to theorem proving in Lean, using the Mathlib library, and building definitions in Lean. No prior experience with Lean is needed: all faculty, PhD scholars and Masters students in the department are welcome! The workshop will be led by Dr. T. V. H. Prathamesh, Assistant Professor of Computer Science, Krea University.
To get a feel for theorem proving in Lean, we will organize mini-seminars from 23rd to 25th February where we will play the Natural Number Game, and get started with installing Lean.
Please fill in this Google Form to indicate your interest in participating in the workshop: https://forms.gle/2MhdGHZWcHyUEqXN7
Below is a brief outline of the topics that will be covered during the workshop:
1. Thursday Afternoon (26th Feb) in LHC-II (103) from 4:00 PM to 7:00 PM:
Below is a brief outline of the topics that will be covered during the workshop:
1. Thursday Afternoon (26th Feb) in LHC-II (103) from 4:00 PM to 7:00 PM:
a. Talk:
Title: Introducing Lean; What it is, Why it matters, and How it works?
Duration: 1 hour
b. Tutorial:
Title: Introduction to Proving in Lean
Duration: 2 hours
2. Friday Morning (27th Feb) in ME115 from 9:15 AM to 1:00 PM:
Title: Introducing Lean; What it is, Why it matters, and How it works?
Duration: 1 hour
b. Tutorial:
Title: Introduction to Proving in Lean
Duration: 2 hours
2. Friday Morning (27th Feb) in ME115 from 9:15 AM to 1:00 PM:
a. Tutorial:
Title: Proving in Lean 1: Basic Tactics
Duration: 3 hours
b. Talk:
Title: Navigating Lean: Mathlib Library, Projects in Lean, and Other Documentation.
Duration: 30 mins (towards the later half or the end of the session)
3. Friday Afternoon (27th Feb) in LHC-II (103) from 2:30 PM to 6:00 PM:
Title: Proving in Lean 1: Basic Tactics
Duration: 3 hours
b. Talk:
Title: Navigating Lean: Mathlib Library, Projects in Lean, and Other Documentation.
Duration: 30 mins (towards the later half or the end of the session)
3. Friday Afternoon (27th Feb) in LHC-II (103) from 2:30 PM to 6:00 PM:
a. Tutorial
Title: Proving in Lean 2: Intermediate Tactics
Duration: 3 hours
b. Talk:
Title: Demystifying Lean: A Type Theory Primer for Tactics and Blackboxes.
Duration: 30 minutes
4. Saturday Morning (28th Feb) in LHC-II (103) from 9:30 PM to 1:00 PM:
Title: Proving in Lean 2: Intermediate Tactics
Duration: 3 hours
b. Talk:
Title: Demystifying Lean: A Type Theory Primer for Tactics and Blackboxes.
Duration: 30 minutes
4. Saturday Morning (28th Feb) in LHC-II (103) from 9:30 PM to 1:00 PM:
a. Tutorial
Title: Definitions, Structures and Programs in Lean
Duration: 3 hours
b. Talk:
Title: What Next? Open Projects and Future Directions, Teaching with Lean
Duration: 30 minutes"
Title: Definitions, Structures and Programs in Lean
Duration: 3 hours
b. Talk:
Title: What Next? Open Projects and Future Directions, Teaching with Lean
Duration: 30 minutes"
