doc: Add a warning mentioning Lean 4 to the readme (#19243)

Also correct links to point to the lean3 webpages; this means that users clicking them end up on pages which also have scary banners telling them not to use Lean 3.

Author: eric-wieser

README.md

@@ -1,28 +1,32 @@
-# Lean mathlib
+# Lean 3's mathlib
+
+> [!WARNING]  
+> Lean 3 and Mathlib 3 are no longer actively maintained.
+> It is strongly recommended that you use [mathlib4](https://github.com/leanprover-community/mathlib4) for Lean 4 instead.
 
 ![](https://github.com/leanprover-community/mathlib/workflows/continuous%20integration/badge.svg?branch=master)
 [![Bors enabled](https://bors.tech/images/badge_small.svg)](https://app.bors.tech/repositories/24316)
 [![project chat](https://img.shields.io/badge/zulip-join_chat-brightgreen.svg)](https://leanprover.zulipchat.com)
 [![Gitpod Ready-to-Code](https://img.shields.io/badge/Gitpod-ready--to--code-blue?logo=gitpod)](https://gitpod.io/#https://github.com/leanprover-community/mathlib)
 
-[Mathlib](https://leanprover-community.github.io) is a user maintained library for the [Lean theorem prover](https://leanprover.github.io).
+[Mathlib](https://leanprover-community.github.io) is a user maintained library for the [Lean 3 theorem prover](https://github.com/leanprover-community/lean).
 It contains both programming infrastructure and mathematics,
 as well as tactics that use the former and allow to develop the latter.
 
 ## Installation
 
-You can find detailed instructions to install Lean, mathlib, and supporting tools on [our website](https://leanprover-community.github.io/get_started.html).
+You can find detailed instructions to install Lean 3, mathlib 3, and supporting tools on [our website](https://leanprover-community.github.io/lean3/get_started.html).
 
 ## Experimenting
 
-Got everything installed? Why not start with the [tutorial project](https://leanprover-community.github.io/install/project.html)?
+Got everything installed? Why not start with the [tutorial project](https://leanprover-community.github.io/lean3/install/project.html)?
 
-For more pointers, see [Learning Lean](https://leanprover-community.github.io/learn.html).
+For more pointers, see [Learning Lean](https://leanprover-community.github.io/lean3/learn.html).
 
 ## Documentation
 
 Besides the installation guides above and [Lean's general
-documentation](https://leanprover.github.io/documentation/), the documentation
+documentation](https://leanprover.github.io/lean3/documentation/), the documentation
 of mathlib consists of:
 
 - [The mathlib docs](https://leanprover-community.github.io/mathlib_docs): documentation [generated
@@ -33,10 +37,10 @@ of mathlib consists of:
   - [hole commands](https://leanprover-community.github.io/mathlib_docs/hole_commands.html), and
   - [attributes](https://leanprover-community.github.io/mathlib_docs/attributes.html).
 - A description of [currently covered theories](https://leanprover-community.github.io/theories.html),
-  as well as an [overview](https://leanprover-community.github.io/mathlib-overview.html) for mathematicians.
+  as well as an [overview](https://leanprover-community.github.io/lean3/mathlib-overview.html) for mathematicians.
 - A couple of [tutorial Lean files](docs/tutorial/)
-- Some [extra Lean documentation](https://leanprover-community.github.io/learn.html) not specific to mathlib (see "Miscellaneous topics")
-- Documentation for people who would like to [contribute to mathlib](https://leanprover-community.github.io/contribute/index.html)
+- Some [extra Lean documentation](https://leanprover-community.github.io/lean3/learn.html) not specific to mathlib (see "Miscellaneous topics")
+- Documentation for people who would like to [contribute to mathlib3](https://leanprover-community.github.io/lean3/contribute/index.html)
 
 Much of the discussion surrounding mathlib occurs in a
 [Zulip chat room](https://leanprover.zulipchat.com/). Since this
@@ -49,8 +53,11 @@ welcomed.
 
 ## Contributing
 
+> [!WARNING]  
+> Contributions are no longer accepted to mathlib 3; contribute to mathlib 4 instead!
+
 The complete documentation for contributing to ``mathlib`` is located
-[on the community guide contribute to mathlib](https://leanprover-community.github.io/contribute/index.html)
+[on the community guide contribute to mathlib](https://leanprover-community.github.io/lean3/contribute/index.html)
 
 The process is different from other projects where one should not fork the repository.
 Instead write permission for non-master branches should be requested on [Zulip](https://leanprover.zulipchat.com)
@@ -60,9 +67,9 @@ by introducing yourself, providing your GitHub handle and what contribution you
 
 Mathlib has the following guidelines and conventions that must be followed
 
- - The [style guide](https://leanprover-community.github.io/contribute/style.html)
- - A guide on the [naming convention](https://leanprover-community.github.io/contribute/naming.html)
- - The [documentation style](https://leanprover-community.github.io/contribute/doc.html)
+ - The [style guide](https://leanprover-community.github.io/lean3/contribute/style.html)
+ - A guide on the [naming convention](https://leanprover-community.github.io/lean3/contribute/naming.html)
+ - The [documentation style](https://leanprover-community.github.io/lean3/contribute/doc.html)
  - The [commit naming conventions](https://github.com/leanprover-community/lean/blob/master/doc/commit_convention.md)
 
 Note: the title of a PR should follow the commit naming convention.