diff --git a/README.md b/README.md
index 552f2da..8c6d2e6 100644
--- a/README.md
+++ b/README.md
@@ -18,6 +18,8 @@ NeurIPS (Datasets and Benchmarks Track), 2023, Oral presentation
 }
 ```
 
+Lean 3 is deprecated. The `main` branch only supports Lean 4. You may use the [`legacy`](https://github.com/lean-dojo/ReProver/tree/legacy) branch if you want to work with Lean 3.
+
 [![GitHub license](https://img.shields.io/github/license/MineDojo/MineDojo)](https://github.com/MineDojo/MineDojo/blob/main/LICENSE) [![Code style: black](https://img.shields.io/badge/code%20style-black-000000.svg)](https://github.com/psf/black)