Lean as a Language: Getting Started

Meetup 1 — Lean as a Language: Getting Started
A welcoming entry point — no prior Lean experience required. We'll make sure everyone leaves with a working development environment (the `elan` toolchain and the VS Code extension). The focus is Lean as a practical, modern functional programming language: evaluating expressions, defining functions and data types, working with structures, and letting the type checker guide your work. Expect a hands-on, low-pressure evening aimed at building fluency and momentum before any theorem proving enters the picture.

Reading (before the meetup)

• FPiL: Functional Programming in Lean Ch 1–2: Getting to Know Lean → Hello, World!
• TPiL: Dependent Type Theory Ch 2: Dependent Type Theory — skim for intuition only

In session

• Evaluating expressions, types, functions, `structure`, inductive datatypes & pattern matching, polymorphism.
• Running a first program with `lake`.

Exercises - FPiL — Getting to Know Lean
— Ex 2, 4 (§1.3 Functions and Definitions), Ex 7 (§1.4 Structures), Ex 11, 14, 15 (§1.6 Polymorphism)