Add some Lean resources to diary

tex/forest.bib

@@ -717,13 +717,13 @@ @misc{browne2012grassmann
 }
 
 @misc{loret2024universe,
-      title={The universe is not a Lie, but actually an Hopf, algebra}, 
+      title={The universe is not a Lie, but actually an Hopf, algebra},
       author={Niccoló Loret},
       year={2024},
       eprint={2408.16970},
       archivePrefix={arXivs},
       primaryClass={gr-qc},
-      url={https://arxiv.org/abs/2408.16970}, 
+      url={https://arxiv.org/abs/2408.16970},
 }
 
 @book{ahle2024tensor,
@@ -735,13 +735,13 @@ @book{ahle2024tensor
 }
 
 @misc{henry2024geometry,
-      title={Geometry of Lightning Self-Attention: Identifiability and Dimension}, 
+      title={Geometry of Lightning Self-Attention: Identifiability and Dimension},
       author={Nathan W. Henry and Giovanni Luca Marchetti and Kathlén Kohn},
       year={2024},
       eprint={2408.17221},
       archivePrefix={arXiv},
       primaryClass={cs.LG},
-      url={https://arxiv.org/abs/2408.17221}, 
+      url={https://arxiv.org/abs/2408.17221},
 }
 
 @article{hamilton2023supergeometric,
@@ -965,13 +965,13 @@ @book{love2024role
 }
 
 @misc{quevedo2024cambridge,
-      title={Cambridge Lectures on The Standard Model}, 
+      title={Cambridge Lectures on The Standard Model},
       author={Fernando Quevedo and Andreas Schachner},
       year={2024},
       eprint={2409.09211},
       archivePrefix={arXiv},
       primaryClass={hep-th},
-      url={https://arxiv.org/abs/2409.09211}, 
+      url={https://arxiv.org/abs/2409.09211},
 }
 
 @book{faddeev2009lectures,
@@ -1020,3 +1020,11 @@ @book{pinkall2024differential
   publisher={Springer Nature},
   url={https://olligross.github.io/projects/DGCS/DGCS_project.html}
 }
+
+@inproceedings{massot2024teaching,
+  title={Teaching Mathematics Using Lean and Controlled Natural Language},
+  author={Massot, Patrick},
+  booktitle={15th International Conference on Interactive Theorem Proving (ITP 2024)},
+  year={2024},
+  organization={Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik}
+}

trees/refs/massot2024teaching.tree

@@ -0,0 +1,15 @@
+% ["forest"]
+\title{Teaching mathematics using lean and controlled natural language}
+\date{2024}
+\author{Patrick Massot}
+\taxon{reference}
+
+\meta{bibtex}{\startverb
+@inproceedings{massot2024teaching,
+ title = {Teaching Mathematics Using Lean and Controlled Natural Language},
+ author = {Massot, Patrick},
+ year = {2024},
+ booktitle = {15th International Conference on Interactive Theorem Proving (ITP 2024)},
+ organization = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik}
+}
+\stopverb}

trees/uts-0018.tree

@@ -14,6 +14,13 @@
 \subtree[2024-09]{
 \title{September, 2024}
 
+\mdblock{09-27}{
+- found \citek{massot2024teaching}
+- noticed that [Scientific Computing in Lean](https://lecopivo.github.io/scientific-computing-lean/) is now written in Verso!
+- checked some progress in [Type Checking in Lean 4](https://ammkrn.github.io/type_checking_in_lean4/)
+- I should put together a list of resources for learning Lean, as I have been asked and answered this question multiple times
+}
+
 \mdblock{09-26}{
 
 - add [[uts-001N]]
@@ -234,7 +241,7 @@ The readings during this period are reflected in
 \subtree[2023-09~12]{
 \title{September to December, 2023}
 \md{
-I was working on Lean related projects during this period, my readings are partially reflected in my [Lean 4 Playground](https://utensil.github.io/lean-playground/).
+I was working on Lean related projects during this period, my readings are partially reflected in my [Lean 4 Playground](https://utensil.github.io/lean-playground/), but most of the time I was reading [Lean's Zulip Chat messages](https://leanprover.zulipchat.com/). Maybe one day I should archive my stars on Zulip Chat.
 }
 }
 \subtree[2023-02~08]{