diff --git a/README.md b/README.md
index a4e15659ce..49a5704ebf 100644
--- a/README.md
+++ b/README.md
@@ -2,19 +2,19 @@ This is the repository for **Lean 4**.
 
 # About
 
-- [Quickstart](https://lean-lang.org/documentation/setup/)
+- [Quickstart](https://lean-lang.org/install/)
 - [Homepage](https://lean-lang.org)
 - [Theorem Proving Tutorial](https://lean-lang.org/theorem_proving_in_lean4/)
 - [Functional Programming in Lean](https://lean-lang.org/functional_programming_in_lean/)
-- [Documentation Overview](https://lean-lang.org/documentation/)
+- [Documentation Overview](https://lean-lang.org/learn/)
 - [Language Reference](https://lean-lang.org/doc/reference/latest/)
 - [Release notes](RELEASES.md) starting at v4.0.0-m3
-- [Examples](https://lean-lang.org/lean4/doc/examples.html)
+- [Examples](https://lean-lang.org/examples/)
 - [External Contribution Guidelines](CONTRIBUTING.md)
 
 # Installation
 
-See [Setting Up Lean](https://lean-lang.org/documentation/setup/).
+See [Install Lean](https://lean-lang.org/install/).
 
 # Contributing
 
diff --git a/src/Lean/Expr.lean b/src/Lean/Expr.lean
index c2b34bd068..a99da227aa 100644
--- a/src/Lean/Expr.lean
+++ b/src/Lean/Expr.lean
@@ -70,7 +70,7 @@ def bar ⦃x : Nat⦄ : Nat := x
 #check bar -- bar : ⦃x : Nat⦄ → Nat
 ```
 
-See also [the Lean manual](https://lean-lang.org/lean4/doc/expressions.html#implicit-arguments).
+See also [the Lean Language Reference](https://lean-lang.org/doc/reference/latest/Terms/Functions/#implicit-functions).
 -/
 inductive BinderInfo where
   /-- Default binder annotation, e.g. `(x : α)` -/
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 30736df07b..70e2312d36 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -568,7 +568,7 @@ Being borrowed only affects the ABI and runtime behavior of the function when co
 
 When a function argument is borrowed, the function does not consume the value. This means that the function will not decrement the value's reference count or deallocate it, and the caller is responsible for doing so.
 
-Please see https://lean-lang.org/lean4/doc/dev/ffi.html#borrowing for a complete description.
+Please see https://lean-lang.org/doc/reference/latest/find/?domain=Verso.Genre.Manual.section&name=ffi-borrowing for a complete description.
 -/
 @[builtin_term_parser] def borrowed   := leading_parser
   "@& " >> termParser leadPrec
diff --git a/src/Lean/Widget/Types.lean b/src/Lean/Widget/Types.lean
index 71ea3c5967..0f60ecdd2f 100644
--- a/src/Lean/Widget/Types.lean
+++ b/src/Lean/Widget/Types.lean
@@ -44,7 +44,7 @@ or use a value of `javascript` identical to that of another definition
 annotated with `@[widget_module]`.
 This makes it possible for the infoview to load the module.
 
-See the [manual entry](https://lean-lang.org/lean4/doc/examples/widgets.lean.html)
+See the [manual entry](https://lean-lang.org/examples/1900-1-1-widgets/)
 for more information on how to use the widgets system. -/
 structure Module where
   /-- A JS [module](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Guide/Modules)