update

pitmonticone · Jun 14, 2024 · a6bb907 · a6bb907
1 parent d4582c1
commit a6bb907
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 27 deletions.
diff --git a/README.md b/README.md
@@ -41,16 +41,4 @@ To actually build the blueprint, run
 lake exe cache get
 lake build
 inv all
-```
-
-## Main References
-
-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/).
-7. De Moura and Ullrich. [*The Lean 4 Theorem Prover and Programming Language*](https://doi.org/10.1007/978-3-030-79876-5_37).
-8. Buzzard. [*The Fermat's Last Theorem Project*](https://leanprover-community.github.io/blog/posts/FLT-announcement/).
-9. Lowry-Duda. [*FLT3 at Lean for the Curious Mathematician 2024*](https://davidlowryduda.com/flt3-at-lftcm2024/).
+```
diff --git a/blueprint/src/references.bib b/blueprint/src/references.bib
@@ -73,6 +73,12 @@ @article{Avigad2021
 	journal      = {Bulletin of the American Mathematical Society},
 	url          = {http://dx.doi.org/10.1090/bull/1726}
 }
+@article{Massot2021,
+	title        = {Why Formalize Mathematics?},
+	author       = {Massot,  Patrick},
+	year         = {2021},
+	url          = {https://www.imo.universite-paris-saclay.fr/~patrick.massot/files/exposition/why_formalize.pdf}
+}
 @book{Avigad2022,
 	title        = {Mathematical Logic and Computation},
 	author       = {Avigad,  Jeremy},

diff --git a/docs/index.md b/docs/index.md
@@ -41,17 +41,4 @@ To actually build the blueprint, run
 lake exe cache get
 lake build
 inv all
-```
-
-## Main References
-
-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/).
-7. De Moura and Ullrich. [*The Lean 4 Theorem Prover and Programming Language*](https://doi.org/10.1007/978-3-030-79876-5_37).
-8. Limperg and From. [*Aesop: White-Box Best-First Proof Search for Lean*](http://dx.doi.org/10.1145/3573105.3575671).
-9. Buzzard. [*Lean in 2024*](https://xenaproject.wordpress.com/2024/01/20/lean-in-2024/).
-10. Lowry-Duda. [*FLT3 at Lean for the Curious Mathematician 2024*](https://davidlowryduda.com/flt3-at-lftcm2024/).
+```