diff --git a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises2.lean b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises2.lean
index f3ecacd..13edbaa 100644
--- a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises2.lean
+++ b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises2.lean
@@ -1,6 +1,7 @@
-/- Exercises 2
- -
- - Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
+/-
+# References
+
+1. Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
 -/
 
 -- Exercise 1
diff --git a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises3.lean b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises3.lean
index 3c94d41..0f69765 100644
--- a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises3.lean
+++ b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises3.lean
@@ -1,6 +1,7 @@
-/- Exercises 3
- -
- - Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
+/-
+# References
+
+1. Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
 -/
 
 -- Exercise 1
diff --git a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises4.lean b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises4.lean
index 2b53657..d016adc 100644
--- a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises4.lean
+++ b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises4.lean
@@ -1,6 +1,7 @@
-/- Exercises 4
- -
- - Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
+/-
+# References
+
+1. Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
 -/
 
 -- Exercise 1
diff --git a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises5.lean b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises5.lean
index d1a1ec8..e269ec1 100644
--- a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises5.lean
+++ b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises5.lean
@@ -1,6 +1,7 @@
-/- Exercises 5
- -
- - Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
+/-
+# References
+
+1. Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
 -/
 
 -- Exercise 1
diff --git a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean
index 5ffd3a1..84c6fb0 100644
--- a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean
+++ b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises7.lean
@@ -1,6 +1,7 @@
-/- Exercises 7
- -
- - Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
+/-
+# References
+
+1. Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
 -/
 
 -- Exercise 1
diff --git a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises8.lean b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises8.lean
index 33ea728..934b394 100644
--- a/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises8.lean
+++ b/bookshelf/theorem-proving-in-lean/TheoremProvingInLean/Exercises8.lean
@@ -1,6 +1,7 @@
-/- Exercises 8
- -
- - Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
+/-
+# References
+
+1. Avigad, Jeremy. ‘Theorem Proving in Lean’, n.d.
 -/
 
 -- Exercise 1