/LeanInVienna2024

Repository hosting resources for the "Lean Tutorial in Vienna" at TU Wien from September 18 to 20, 2024.

Primary LanguageLeanApache License 2.0Apache-2.0

Lean Tutorial in Vienna (September 18–20, 2024)

Vienna

Installing VS Code

VS Code is the recommended IDE for working with Lean 4. To install VS Code, follow these steps:

  1. Visit the official VS Code website.
  2. Download the latest version of VS Code for your operating system (Windows, macOS, or Linux).
  3. Follow the installation instructions provided on the website to complete the setup process.

Once the installation is complete, you can proceed with configuring VS Code for Lean 4 development.

Installing Lean 4

To install Lean 4, please follow these instructions:

  1. Install the Lean 4 Extension in VS Code:

    • Open VS Code.
    • Navigate to the Extensions sidebar by clicking on the square icon on the left panel.
    • Search for Lean 4 in the search bar and install the Lean 4 extension.

    Installing the vscode-lean4 extension

  2. Access the Lean 4 Setup Guide:

    • Create a new text file by selecting File > New Text File or using the keyboard shortcut (Ctrl + N on Windows/Linux or Cmd + N on macOS).
    • Click on the $\forall$-symbol located in the top right corner of the window.
    • From the dropdown menu, select Documentation… > Docs: Show Setup Guide.

    Docs: Show Setup Guide

  3. Follow the Instructions in the Setup Guide:

    • Carefully read and follow the instructions provided in the Lean 4 setup guide to complete the installation process.

    Setup Guide

Cloning this Repository

To clone this repository, run the following command:

git clone https://github.com/pitmonticone/LeanInVienna2024.git

For detailed instructions, please refer to the GitHub documentation on cloning repositories.

After successfully cloning the repository, navigate into the project directory and execute the following command to retrieve the necessary cached dependencies:

cd LeanInVienna2024/
lake exe cache get

Schedule

Date Time Speaker Topic
Sep 18 09:00 - 10:00 Markus Himmel Introduction to Lean
10:30 - 12:00 Pietro Monticone Installation and Basics
13:30 - 14:15 Tomáš Skřivan Scientific Computing in Lean
14:15 - 15:30 Pietro Monticone Logic (1/2)
16:00 - 17:30 Pietro Monticone Logic (2/2)
Sep 19 9:00 - 09:45 Moritz Firsching Beginner's mistakes using Mathlib/Lean
10:15 - 12:15 Markus Himmel Sets and Functions
13:45 - 14:30 Markus Himmel Working with Mathlib
14:30 - 15:45 Moritz Firsching Elementary Number Theory (1/2)
16:15 - 17:30 Moritz Firsching Elementary Number Theory (2/2)
Sep 20 09:00 - 09:30 Markus Himmel Lean Metaprogramming Overview
09:30 - 10:30 Tomáš Skřivan Structures (1/2)
11:00 - 12:15 Tomáš Skřivan Structures (2/2)
13:45 - 14:30 Pietro Monticone Getting Started with Blueprint-Driven Formalisation Projects in Lean
14:30 - 15:45 Tomáš Skřivan Differential Calculus (1/2)
16:15 - 17:30 Tomáš Skřivan Differential Calculus (2/2)

Search Engines

References