文件列表:

.devcontainer/ (0, 2023-11-15)
.devcontainer/Dockerfile (249, 2023-11-15)
.devcontainer/devcontainer.json (428, 2023-11-15)
.docker/ (0, 2023-11-15)
.docker/gitpod/ (0, 2023-11-15)
.docker/gitpod/Dockerfile (1456, 2023-11-15)
HausdorffSchool.lean (57, 2023-11-15)
HausdorffSchool/ (0, 2023-11-15)
HausdorffSchool/Common.lean (10164, 2023-11-15)
HausdorffSchool/Session1_Basics/ (0, 2023-11-15)
HausdorffSchool/Session1_Basics/01Calculating.lean (7243, 2023-11-15)
HausdorffSchool/Session1_Basics/S03_Using_Theorems_and_Lemmas.lean (4244, 2023-11-15)
HausdorffSchool/Session1_Basics/S04_More_on_Order_and_Divisibility.lean (1752, 2023-11-15)
HausdorffSchool/Session1_Basics/S05_Proving_Facts_about_Algebraic_Structures.lean (2516, 2023-11-15)
HausdorffSchool/Session1_Basics/Tutorial.lean (4250, 2023-11-15)
HausdorffSchool/Session1_Basics/solutions/ (0, 2023-11-15)
HausdorffSchool/Session1_Basics/solutions/Solutions_Calculating.lean (7718, 2023-11-15)
HausdorffSchool/Session1_Basics/solutions/Solutions_S03_Using_Theorems_and_Lemmas.lean (1716, 2023-11-15)
HausdorffSchool/Session1_Basics/solutions/Solutions_S04_More_on_Order_and_Divisibility.lean (2537, 2023-11-15)
HausdorffSchool/Session1_Basics/solutions/Solutions_S05_Proving_Facts_about_Algebraic_Structures.lean (3279, 2023-11-15)
HausdorffSchool/Session2_Sets_Fns_Logic/ (0, 2023-11-15)
HausdorffSchool/Session2_Sets_Fns_Logic/Exercises1.lean (2698, 2023-11-15)
HausdorffSchool/Session2_Sets_Fns_Logic/Exercises2.lean (2767, 2023-11-15)
HausdorffSchool/Session2_Sets_Fns_Logic/Solutions/ (0, 2023-11-15)
HausdorffSchool/Session2_Sets_Fns_Logic/Solutions/Solutions_Exercises1.lean (3636, 2023-11-15)
HausdorffSchool/Session2_Sets_Fns_Logic/Solutions/Solutions_Exercises2.lean (5725, 2023-11-15)
HausdorffSchool/Session2_Sets_Fns_Logic/Tutorial1.lean (3432, 2023-11-15)
HausdorffSchool/Session2_Sets_Fns_Logic/Tutorial2.lean (3128, 2023-11-15)
HausdorffSchool/Session3_Topology/ (0, 2023-11-15)
HausdorffSchool/Session3_Topology/S01_Filters.lean (3083, 2023-11-15)
HausdorffSchool/Session3_Topology/S02_Metric_Spaces.lean (7884, 2023-11-15)
HausdorffSchool/Session3_Topology/S03_Topological_Spaces.lean (5157, 2023-11-15)
HausdorffSchool/Session3_Topology/Tutorial.lean (8095, 2023-11-15)
HausdorffSchool/Session3_Topology/solutions/ (0, 2023-11-15)
HausdorffSchool/Session3_Topology/solutions/Solutions_S01_Filters.lean (2922, 2023-11-15)
HausdorffSchool/Session3_Topology/solutions/Solutions_S02_Metric_Spaces.lean (15387, 2023-11-15)
HausdorffSchool/Session3_Topology/solutions/Solutions_S03_Topological_Spaces.lean (8007, 2023-11-15)
HausdorffSchool/Session4_Calculus/ (0, 2023-11-15)
... ...

# Hausdorff School on Lean This is the repository for the Lean sessions of the September 2023 Hausdorff School in Bonn. ## To install Lean Do the following: * Install Lean 4 and VS Code following these [instructions](https://leanprover-community.github.io/get_started.html). * Open a new terminal (we recommend `git bash` on Windows, which was installed as part of git in the first step). * Go the the directory where you would like this package to live. * Run `git clone https://github.com/fpvandoorn/HausdorffSchoolLean.git`. * Run `cd HausdorffSchoolLean` * Run `lake exe cache get` * On Windows, if you get an error that starts with `curl: (35) schannel: next InitializeSecurityContext failed` it is probably your antivirus program that doesn't like that we're downloading many files. The easiest solution is to temporarily disable your antivirus program. * Launch VS Code, either through your application menu or by typing `code .`. (MacOS users need to take a one-off [extra step](https://code.visualstudio.com/docs/setup/mac#_launching-from-the-command-line) to be able to launch VS Code from the command line.) * If you launched VS Code from a menu, on the main screen, or in the File menu, click "Open folder" (just "Open" on a Mac), and choose the folder `HausdorffSchoolLean` (*not* one of its subfolders). * Test that everything is working by opening `HausdorffSchool/Test.lean`. It is normal if it takes 10-40 seconds for Lean to start up. * More files will be added to this repository during the tutorial. The first exercises are in `HausdorffSchool/Session1_Basics/01Calculating.lean`. ## Get new exercises If you have already followed the steps above, and want to get the latest exercises, open a terminal in your local copy of this repository (e.g. `cd HausdorffSchoolLean`) and then run `git pull`. This gives you the new exercises. ## Setting up Codespaces If you have trouble installing Lean, you can use Lean directly in your browser using Github codespaces. This requires a Github account. If you are signed in to Github, click here: * Make sure the Machine type is `4-core`, and then press `Create codespace` * After 1-2 minutes you see a VSCode window in your browser. However, it is still busily downloading mathlib in the background, so give it another few minutes (5 to be safe) and then open a `.lean` file to start. ## To use this repository with Gitpod Gitpod is an alternative to codespaces that is slightly inconvenient, since it requires you to verify your phone number. Click this button to get started: [](https://gitpod.io/#https://github.com/fpvandoorn/HausdorffSchoolLean) This creates a virtual machine in the cloud, and installs Lean and Mathlib. It then presents you with a VS Code window, running in a virtual copy of the repository. You can update the repository by opening a terminal in the browser and typing `git pull` followed by `lake exe cache get` as above. Gitpod gives you 50 free hours every month. When you are done working, choose `Stop workspace` from the menu on the left. The workspace should also stop automatically 30 minutes after the last interaction or 3 minutes after closing the tab. To restart a previous workspace, go to [https://gitpod.io/workspaces/](https://gitpod.io/workspaces/). ## More information You can find the textbook that we will use online in [html format](https://leanprover-community.github.io/mathematics_in_lean/) or as a [pdf document](https://leanprover-community.github.io/mathematics_in_lean/mathematics_in_lean.pdf).

近期下载者：

相关文件：

评论：[我要评论] [举报此文件]

收藏者：