diff --git a/doc/SUMMARY.md b/doc/SUMMARY.md
index 88892f6a18..75f2fface4 100644
--- a/doc/SUMMARY.md
+++ b/doc/SUMMARY.md
@@ -5,7 +5,7 @@
 - [Setting Up Lean](./setup.md)
   - [Quickstart](./quickstart.md)
 
-# [Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean4/title_page.html)
+# [Theorem Proving in Lean](./tpil.md)
 
 # [Examples](./examples.md)
 
diff --git a/doc/tpil.md b/doc/tpil.md
new file mode 100644
index 0000000000..891d29ad38
--- /dev/null
+++ b/doc/tpil.md
@@ -0,0 +1,5 @@
+Theorem Proving in Lean
+=======================
+
+We strongly encourage you to read the book [Theorem Proving in Lean](https://leanprover.github.io/theorem_proving_in_lean4/title_page.html).
+Many Lean users consider it to be the Lean Bible.