Update index.md

docs/index.md

@@ -44,4 +44,21 @@ inv all
 
 ## References
 
-Hindry (2011) [Arithmetics](https://doi.org/10.1007/978-1-4471-2131-2). *Springer*.
+### Books
+
+1. Hindry. [*Arithmetics*](http://dx.doi.org/10.1007/978-1-4471-2131-2).
+2. Avigad and Massot. [*Mathematics in Lean*](https://leanprover-community.github.io/mathematics_in_lean/).
+3. Avigad et al. [*Theorem Proving in Lean 4*](https://leanprover.github.io/theorem_proving_in_lean4/).
+4. Macbeth. [*The Mechanics of Proof*](https://hrmacbeth.github.io/math2001/).
+5. Velleman. [*How To Prove It With Lean*](https://djvelleman.github.io/HTPIwL/).
+6. Christiansen. [*Functional Programming in Lean*](https://lean-lang.org/functional_programming_in_lean/).
+
+### Papers
+
+1. de Moura and Ullrich. [*The Lean 4 Theorem Prover and Programming Language*](https://doi.org/10.1007/978-3-030-79876-5_37).
+2. Limperg and From. [*Aesop: White-Box Best-First Proof Search for Lean*](http://dx.doi.org/10.1145/3573105.3575671).
+
+### Blog Posts
+
+1. Buzzard. [*Lean in 2024*](https://xenaproject.wordpress.com/2024/01/20/lean-in-2024/)
+2. Lowry-Duda. [*FLT3 at Lean for the Curious Mathematician 2024*](https://davidlowryduda.com/flt3-at-lftcm2024/).