The readings shared in Mastodon on 7 October 2024 are

• Readings shared October 6, 2024. #ITP #LeanProver #Logic #Math #AI #Python
• Proofs of the pigeonhole principle in Lean4. #ITP #Lean4 #Math #Calculemus
• Formalizing MLTL formula progression in Isabelle/HOL. ~ Katherine Kosaian, Zili Wang, Elizabeth Sloan, Kristin Rozier. #ITP #IsabelleHOL #Logic
• Repo for the first BerLean workshop. #ITP #Lean4 #Math
• Re-invention of group/ring algebra in Lean 4 for learning purposes. ~ Eugene Zolotarev. #ITP #Lean4 #Math
• Introduction to mathematical arguments (background handout for courses requiring proofs). ~ Michael Hutchings. #Logic #Math
• How to write proofs: a quick guide. ~ Eugenia Cheng. #Logic #Math
• Notes on math proof. ~ Bruce Ikenaga. #Logic #Math
• Proof writing and presentation tips. ~ Erika L.C. King. #Logic #Math
• How to write mathematics. ~ Martin Erickson. #Logic #Math
• Advice on mathematical writing. ~ Keith Conrad. #Math
• Examples of proofs by induction. ~ Keith Conrad. #Math
• An introduction to proofs and the mathematical vernacular. ~ Martin V. Day. #Math
• Conventions for writing mathematical proofs. ~ John M. Lee. #Math
• TheoremLlama: Transforming general-purpose LLMs into Lean4 experts. ~ Ruida Wang, Jipeng Zhang, Yizhen Jia, Rui Pan, Shizhe Diao, Renjie Pi, Tong Zhang. #ITP #Lean4 #LLMs