leanprover.github.io -> lean-lang.org (#553)

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

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.

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

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
 

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)
 

templates/index.html

@@ -41,7 +41,7 @@ <h4>Learn to Lean!</h4>
 		</div>
 		<ul class="list-group list-group-flush border-top">
           <li class="list-group-item"><a href="learn.html">Learning resources</a></li>
-          <li class="list-group-item"><a href="https://leanprover.github.io/theorem_proving_in_lean4/"
+          <li class="list-group-item"><a href="https://lean-lang.org/theorem_proving_in_lean4/"
                  >Theorem Proving in Lean 4</a> (an introduction)</li>
           <li class="list-group-item"><a href="https://leanprover-community.github.io/mathlib4_docs"
                  >API documentation of mathlib</a></li>

templates/learn.md

@@ -24,10 +24,10 @@ Some have Lean 3 versions, but there is no point learning Lean 3 at this stage.
   using Lean, and then independent topic files about elementary analysis,
   abstract topology and mathematical logic.
 
-* If you wish to learn directly from source, the 
-  [Lean API documentation](https://leanprover-community.github.io/mathlib4_docs/) 
-  not only includes `Mathlib`, but also covers `Std`, `Batteries`, `Lake`, and the core compiler. 
-  As much of Lean is defined in terms of syntax extensions, this is the closest thing to a 
+* If you wish to learn directly from source, the
+  [Lean API documentation](https://leanprover-community.github.io/mathlib4_docs/)
+  not only includes `Mathlib`, but also covers `Std`, `Batteries`, `Lake`, and the core compiler.
+  As much of Lean is defined in terms of syntax extensions, this is the closest thing to a
   comprehensive reference manual that exists.
 
 ## Books
@@ -48,19 +48,19 @@ doing Lean exercises on the fly:
   experience.
 
 * If you prefer something more about the foundations of type theory, the standard reference is
-  [Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean4/).
+  [Theorem Proving in Lean](https://lean-lang.org/theorem_proving_in_lean4/).
 
 * A computer-science/programming-oriented book is
   [The Hitchhiker's Guide to Logical Verification](https://raw.githubusercontent.com/blanchette/logical_verification_2023/main/hitchhikers_guide.pdf).
   It also has useful information about the type theory of Lean, and an associated VSCode project with exercises.
 
 If you want something more focused on Lean itself than on using Lean, then you
-can read the [reference manual](https://leanprover.github.io/lean4/doc/).
+can read the [reference manual](https://lean-lang.org/lean4/doc/).
 
 ## (Meta)-programming and tactic writing
 
 * If you are interested in Lean as a programming language then you should read
-  [Functional programming in Lean](https://leanprover.github.io/functional_programming_in_lean/).
+  [Functional programming in Lean](https://lean-lang.org/functional_programming_in_lean/).
 
 * If you specifically want to do meta-programming and write tactics then you can read
   [Metaprogramming in Lean 4](https://github.com/arthurpaulino/lean4-metaprogramming-book)
@@ -87,7 +87,7 @@ those of Lean. The most relevant differences to keep in mind are:
   to higher universes.
 * Lean natively supports quotient types and their associated reduction
   rule (see [this
-  section](https://leanprover.github.io/theorem_proving_in_lean4/axioms_and_computation.html#quotients)
+  section](https://lean-lang.org/theorem_proving_in_lean4/axioms_and_computation.html#quotients)
   of *Theorem proving in Lean*).
 
 If you can read the above Coq documentation then you are ready for