From 704989294cbe0592351ed2642bfa0357b1afd909 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 21 Nov 2024 15:07:32 +0100 Subject: [PATCH] leanprover.github.io -> lean-lang.org (#553) --- data/courses.yaml | 10 +++++----- data/presentation.md | 2 +- lean.bib | 2 +- templates/extras/tactic_writing.md | 6 +++--- templates/glossary.md | 20 ++++++++++---------- templates/index.html | 2 +- templates/learn.md | 16 ++++++++-------- 7 files changed, 29 insertions(+), 29 deletions(-) diff --git a/data/courses.yaml b/data/courses.yaml index 37b41d7fd8..bfd3533ac7 100644 --- a/data/courses.yaml +++ b/data/courses.yaml @@ -71,15 +71,15 @@ summary: "Introducing to Lean proofs and programming for scientists and engineers. Prerequisite: Calculus II. Students should learn basic proofs (up to some calculus examples) and basic programming techniques (I/O, functional programming, arrays) to inspire and enable development of scientific computing software connected to formalized scientific derivations in Lean." tags: ['beginner', 'functional programming', 'intro to proof'] website: https://leanprover.zulipchat.com/#narrow/stream/445230-Lean-for-Scientists-and-Engineers-2024/ - experiences: TBD (course being held July through August) + experiences: TBD (course being held July through August) - name: Introduction to Mathematical Formalization instructor: Vasily Ilin institution: University of Washington year: 2024 lean_version: 4 - summary: Project-based course aimed at undergrads and early grad students. The focus of the class was purely on the practical aspect of using Lean to state and prove mathematical statements. The intended outcome was not a deep understanding of how Lean works but having the practical skills of breaking down the problem, debugging it, asking for help on Zulip in a productive way, etc. The students spend the first 3 weeks doing exercises in MiL, and the other 7 weeks doing a project. + summary: Project-based course aimed at undergrads and early grad students. The focus of the class was purely on the practical aspect of using Lean to state and prove mathematical statements. The intended outcome was not a deep understanding of how Lean works but having the practical skills of breaking down the problem, debugging it, asking for help on Zulip in a productive way, etc. The students spend the first 3 weeks doing exercises in MiL, and the other 7 weeks doing a project. tags: ['English', 'mathematics', 'beginner'] - experiences: Students felt that the pace is too fast. No one completed more than 4-5 chapters of MiL. Projects mostly went well. Each team had two people -- a team leader, who proposed the project (grad student or student with previous Lean experience). This worked well in that the team leader moved the project forward but, on the other hand, the other team member struggled to keep up. + experiences: Students felt that the pace is too fast. No one completed more than 4-5 chapters of MiL. Projects mostly went well. Each team had two people -- a team leader, who proposed the project (grad student or student with previous Lean experience). This worked well in that the team leader moved the project forward but, on the other hand, the other team member struggled to keep up. - name: Computergestütztes mathematisches Beweisen instructor: Ralf Gerkmann institution: Ludwig-Maximilians-Universität München @@ -206,7 +206,7 @@ - name: Logic and Proof instructor: Jeremy Avigad institution: Carnegie Mellon University - material: https://leanprover.github.io/logic_and_proof/ + material: https://lean-lang.org/logic_and_proof/ lean_version: 3 tags: ['logic', 'intro to proof'] summary: This is an introduction to logic and mathematical reasoning for a general audience. It was taught in the philosophy department at CMU twice. @@ -377,7 +377,7 @@ instructor: Robert Y. Lewis, Jasmin Blanchette, Anne Baanen institution: Vrije Universiteit Amsterdam website: https://studiegids.vu.nl/en/2022-2023/courses/X_401015 - material: https://leanprover.github.io/logic_and_proof/logic_and_proof.pdf + material: https://lean-lang.org/logic_and_proof/logic_and_proof.pdf tags: ['intro to proof', 'logic', 'computer science'] lean_version: 3 summary: > diff --git a/data/presentation.md b/data/presentation.md index 88f6ff1b49..3edb8ac166 100644 --- a/data/presentation.md +++ b/data/presentation.md @@ -1,6 +1,6 @@ ## Lean and its Mathematical Library -The [Lean theorem prover](https://leanprover.github.io) +The [Lean theorem prover](https://lean-lang.org) is a proof assistant developed principally by Leonardo de Moura. The community recently switched from using Lean 3 to using Lean 4. diff --git a/lean.bib b/lean.bib index 43ea9da84c..e1383ca3a4 100644 --- a/lean.bib +++ b/lean.bib @@ -79,7 +79,7 @@ @Book{ Avig14 author = "Avigad, Jeremy and {de Moura}, Leonardo and Kong, Soonho", title = {{Theorem Proving in Lean}}, year = "2014", - link = "\url{https://leanprover.github.io/tutorial/tutorial.pdf}", + link = "\url{https://lean-lang.org/tutorial/tutorial.pdf}", publisher = "Carnegie Mellon University" } diff --git a/templates/extras/tactic_writing.md b/templates/extras/tactic_writing.md index 84c1304bf0..f8c248a830 100644 --- a/templates/extras/tactic_writing.md +++ b/templates/extras/tactic_writing.md @@ -29,7 +29,7 @@ Other useful resources while learning to write tactics include: Lean for the Curious Mathematician 2020 * Chapter 7 of the [Hitchhiker's Guide to Logical Verification](https://github.com/blanchette/logical_verification_2021/raw/main/hitchhikers_guide.pdf) * the original paper about metaprogramming Lean - [A Metaprogramming Framework for Formal Verification](https://leanprover.github.io/papers/tactic.pdf) + [A Metaprogramming Framework for Formal Verification](https://lean-lang.org/papers/tactic.pdf) ## Monadology @@ -476,8 +476,8 @@ This is the end of this tutorial (although there are two cheat sheets below). If you want to learn more, you can read the definitions of tactics in either the core library or mathlib, see what you can understand, and ask specific questions on Zulip. For more theory, especially a proper explanation of monads, you can read -[Programming in Lean](https://leanprover.github.io/programming_in_lean/), but the actual tactic writing part is not up to date. The official documentation of the tactic framework is -the paper [A Metaprogramming Framework for Formal Verification](https://leanprover.github.io/papers/tactic.pdf). +[Programming in Lean](https://lean-lang.org/programming_in_lean/), but the actual tactic writing part is not up to date. The official documentation of the tactic framework is +the paper [A Metaprogramming Framework for Formal Verification](https://lean-lang.org/papers/tactic.pdf). ## Mario's backtick cheat sheet diff --git a/templates/glossary.md b/templates/glossary.md index 5794c2d302..cfc199aec5 100644 --- a/templates/glossary.md +++ b/templates/glossary.md @@ -43,7 +43,7 @@ The `@[simp]` attribute, for example, tags a declaration (typically a `lemma`, ` * [The mathlib attributes documentation](https://leanprover-community.github.io/mathlib_docs/attributes.html), for a list of those defined and used throughout [mathlib](#mathlib) -* [Section 5.4 of *The Lean Reference Manual*](https://leanprover.github.io/reference/other_commands.html#attributes), for a list of those defined within [core lean](#core-lean) +* [Section 5.4 of *The Lean Reference Manual*](https://lean-lang.org/reference/other_commands.html#attributes), for a list of those defined within [core lean](#core-lean) ### beta reduction @@ -53,7 +53,7 @@ More precisely, it is the process of simplifying an expression such as `(λ x, t ##### See also -* [Section 2.3 of Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html#function-abstraction-and-evaluation) +* [Section 2.3 of Theorem Proving in Lean](https://lean-lang.org/theorem_proving_in_lean/dependent_type_theory.html#function-abstraction-and-evaluation) ### big operators @@ -154,7 +154,7 @@ Or, ambiguously, any of a number of Lean commands which may define or declare su Examples of such commands are the `def`, `theorem`, `constant` or `example` commands (and in Lean 3, the `lemma` command), amongst others. -Further detail can be found in the [Lean documentation](https://leanprover.github.io/lean4/doc/declarations.html#basic-declarations). +Further detail can be found in the [Lean documentation](https://lean-lang.org/lean4/doc/declarations.html#basic-declarations). ### dependent type theory @@ -164,7 +164,7 @@ Lean's implementation of dependent type theory is based on what is known as the ##### See Also -* [Section 2 of Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html), which discusses Lean's specific version of dependent type theory +* [Section 2 of Theorem Proving in Lean](https://lean-lang.org/theorem_proving_in_lean/dependent_type_theory.html), which discusses Lean's specific version of dependent type theory * [Calculus of Constructions, from Wikipedia](https://en.wikipedia.org/wiki/Calculus_of_constructions), for a further overview of the calculus of constructions @@ -313,7 +313,7 @@ A deprecated mathematics library for Lean 3. A [tool](https://github.com/leanprover/mathport/) for automated or semi-automated translation of Lean 3 code into Lean 4 code. It consists of both fully automated generation of Lean 4 [olean files](#olean-file) from Lean 3 source files (*binport*), as well as best-effort source-to-source translation of Lean 3 to Lean 4 source code (*synport*). -Learnings from both the mathport effort as well as from [mathlib4](#mathlib4) often lead to backported changes to mathlib, to bring Lean 3 code into more future-compatible states. +Learnings from both the mathport effort as well as from [mathlib4](#mathlib4) often lead to backported changes to mathlib, to bring Lean 3 code into more future-compatible states. ### mode @@ -397,14 +397,14 @@ Allowed style linting exceptions are stored in a [style exceptions file](https:/ ### tactic mode A Lean [mode](#mode) characterized by its reliance on sequences of [tactics](#tactic) which often facilitate proofs quite similar to paper-based reasoning, albeit often with the use of sophisticated tactics which automate tedious portions of a proof. -There are various means to [enter tactic mode](https://leanprover.github.io/theorem_proving_in_lean/tactics.html#entering-tactic-mode). +There are various means to [enter tactic mode](https://lean-lang.org/theorem_proving_in_lean/tactics.html#entering-tactic-mode). It may be entered using the `by` keyword from [term mode](#term-mode), though in Lean 3 it is most often entered via a `begin...end` block whenever its body is made up of multiple commands. Other modes can also be interspersed within it, often to collaboratively produce an understandable, efficient, short or readable overall proof. Ultimately, the result of a tactic mode block is a [term](#term), assembled via the tactics within it. ##### See also -* [Section 5 of Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean/tactics.html), which discusses tactics, as well as moving into and out of tactic mode +* [Section 5 of Theorem Proving in Lean](https://lean-lang.org/theorem_proving_in_lean/tactics.html), which discusses tactics, as well as moving into and out of tactic mode * [The `show_term` tactic](https://leanprover-community.github.io/mathlib_docs/tactic/show_term.html) which can reveal the assembled [term](#term) @@ -422,8 +422,8 @@ Commands such as `have`, `suffices`, and `show` can be used to write structured ### TPIL -"[Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean/index.html)", a free online textbook by Jeremy Avigad, Leonardo de Moura, and Soonho Kong, "designed to teach you to develop and verify proofs in Lean". -Starting with a simple introduction to the [type theory](https://leanprover.github.io/theorem_proving_in_lean/dependent_type_theory.html) used in Lean, the text proceeds to explain topics such as [tactics](https://leanprover.github.io/theorem_proving_in_lean/tactics.html), [inductive types](https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html), and [type classes](https://leanprover.github.io/theorem_proving_in_lean/type_classes.html). +"[Theorem Proving in Lean](https://lean-lang.org/theorem_proving_in_lean/index.html)", a free online textbook by Jeremy Avigad, Leonardo de Moura, and Soonho Kong, "designed to teach you to develop and verify proofs in Lean". +Starting with a simple introduction to the [type theory](https://lean-lang.org/theorem_proving_in_lean/dependent_type_theory.html) used in Lean, the text proceeds to explain topics such as [tactics](https://lean-lang.org/theorem_proving_in_lean/tactics.html), [inductive types](https://lean-lang.org/theorem_proving_in_lean/inductive_types.html), and [type classes](https://lean-lang.org/theorem_proving_in_lean/type_classes.html). ### type theory @@ -454,7 +454,7 @@ It also may refer to a command which reduces expressions to this form. ##### See also -* [Section 8.4 of Programming in Lean](https://leanprover.github.io/programming_in_lean/#08_Writing_Tactics.html), which is still in progress, but will cover `whnf` +* [Section 8.4 of Programming in Lean](https://lean-lang.org/programming_in_lean/#08_Writing_Tactics.html), which is still in progress, but will cover `whnf` * [What is weak head normal form? - Stack Overflow](https://stackoverflow.com/questions/6872898/what-is-weak-head-normal-form) * [Weak head normal form - The Haskell wiki](https://wiki.haskell.org/Weak_head_normal_form) diff --git a/templates/index.html b/templates/index.html index d04ff7ed5a..f88ae8009a 100644 --- a/templates/index.html +++ b/templates/index.html @@ -41,7 +41,7 @@

Learn to Lean!