No results found

LeanInVienna

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

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 -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

DateTimeSpeakerTopic
Sep 1809:00 - 10:00Markus HimmelIntroduction to Lean
10:30 - 12:00Pietro MonticoneInstallation and Basics
13:30 - 14:15Tomáš SkřivanScientific Computing in Lean
14:15 - 15:30Pietro MonticoneLogic (1/2)
16:00 - 17:30Pietro MonticoneLogic (2/2)
Sep 199:00 - 09:45Moritz FirschingBeginner's mistakes using Mathlib/Lean
10:15 - 12:15Markus HimmelSets and Functions
13:45 - 14:30Markus HimmelWorking with Mathlib
14:30 - 15:45Moritz FirschingElementary Number Theory (1/2)
16:15 - 17:30Moritz FirschingElementary Number Theory (2/2)
Sep 2009:00 - 09:30Markus HimmelLean Metaprogramming Overview
09:30 - 10:30Tomáš SkřivanStructures (1/2)
11:00 - 12:15Tomáš SkřivanStructures (2/2)
13:45 - 14:30Pietro MonticoneGetting Started with Blueprint-Driven Formalisation Projects in Lean
14:30 - 15:45Tomáš SkřivanDifferential Calculus (1/2)
16:15 - 17:30Tomáš SkřivanDifferential Calculus (2/2)

Search Engines

References