Update 0-introduction.tex

blueprint/src/chapters/0-introduction.tex

@@ -2,13 +2,61 @@ \chapter{Introduction}
 %\label{chap:intro}
 %\addcontentsline{toc}{chapter}{Introduction}
 
+% FORMAL MATHEMATICS RESOURCES
+
+% Projects:
+% - https://leanprover-community.github.io/sphere-eversion/
+% - https://yaeldillies.github.io/LeanAPAP/
+% - https://teorth.github.io/pfr/
+% - https://alexkontorovich.github.io/PrimeNumberTheoremAnd/web/
+% - https://leanprover-community.github.io/flt-regular/blueprint/
+
+% Theses:
+% - https://research.vu.nl/en/publications/formalizing-fundamental-algebraic-number-theory
+
+% Slides:
+% - https://florisvandoorn.com/talks/math_in_lean.pdf
+% - https://florisvandoorn.com/talks/LeanInternals.pdf
+
+% Books:
+% - https://leanprover-community.github.io/mathematics_in_lean/
+% - https://leanprover.github.io/logic_and_proof/
+% - https://leanprover.github.io/theorem_proving_in_lean4/
+% - https://hrmacbeth.github.io/math2001/
+% - https://djvelleman.github.io/HTPIwL/
+% - https://lean-lang.org/functional_programming_in_lean/
+% - https://avigad.github.io/lamr/
+
+% Papers:
+% - https://www.imo.universite-paris-saclay.fr/~patrick.massot/files/exposition/why_formalize.pdf
+% - https://ceur-ws.org/Vol-3377/natfom3.pdf
+% - https://doi.org/10.48550/arXiv.2305.02329
+% - https://cmartinez.web.wesleyan.edu/documents/FP.pdf
+% - https://doi.org/10.1007/978-3-030-79876-5_37
+% - http://dx.doi.org/10.1145/3573105.3575671
+
+% FERMAT'S LAST THEOREM FOR EXPONENT 3
+
+% Books:
+% - http://dx.doi.org/10.1007/978-1-4471-2131-2
+
+% Blog posts:
+% - https://xenaproject.wordpress.com/2024/01/20/lean-in-2024/
+% - https://davidlowryduda.com/flt3-at-lftcm2024/
+
+% CHAPTERS (Tentative)
+% – Introduction: Context, Motivation, Basic Definitions?
+% – Third Cyclotomic Field & Preliminary Results
+% – Fermat’s Last Theorem for Exponent 3: Case 1, Case 2, Conclusion
+% – Acknowledgements / Contributions
+
 % TO SUBMIT
 % – Authors: Pietro Monticone
 % – References: all technical and popular articles and books
 % – Citations: everything (FLT3-Regular, FLT, Mathlib, MIL, formalization in general, etc.)
 % – Introduction: all relevant links and references, main mathematical results, main mathematical methods, main structures, notation, synthesis on formalisation with main benefits, etc.
 % – Motivation: enrich Mathlib, dependency of / used by FLT by Buzzard et al. (Al technical and popular articles)
-% – My contributions: about 20 formalized proofs, all informalised proofs, all blueprint, PR to Mathlib (), Porting to Mathlib, see LaTeX comments
+% – My contributions: about 20 formalized proofs, all informalised proofs, all blueprint, PR to Mathlib (), Porting to Mathlib, see LaTeX comments, talk, ...
 % – Acknowledgements: supervision by Riccardo Brasca (let him see it before submitting), collaboration with my team (see blog post by David)
 
 % TO PUBLISH