The readings shared in Bluesky on 5 August 2025 are

• Simons Foundation Lean Workshop. ~ Antoine Chambert-Loir Alex Kontorovich, Heather MacBeth. #ITP #LeanProver #Math
• First analysis lecture (June 16, 2025) ~ Alex Kontorovich. #ITP #LeanProver #Math
• Doing elementary number theory in Lean. ~ Antoine Chambert-Loir #ITP #LeanProver #Math
• Doing elementary number theory in Lean (Video 1). ~ Antoine Chambert-Loir #ITP #LeanProver #Math
• Doing elementary number theory in Lean (Video 2). ~ Antoine Chambert-Loir #ITP #LeanProver #Math
• First geometry lecture (June 17, 2025). ~ Heather Macbeth. #ITP #LeanProver #Math
• Second geometry lecture (June 18, 2025). ~ Heather Macbeth. #ITP #LeanProver #Math
• Second analysis lecture "Filter" (June 17, 2025) ~ Alex Kontorovich. #ITP #LeanProver #Math
• A crash course on type theory. ~ Antoine Chambert-Loir. #ITP #LeanProver #TypeTheory
• A crash course on type theory (Video). ~ Antoine Chambert-Loir. #ITP #LeanProver #TypeTheory
• Structures in Lean4 (June 20, 2025). ~ Filippo Nuccio. #ITP #LeanProver
• Blueprints and PNT (June 23, 2025). ~ Alex Kontorovich. #ITP #LeanProver
• Simple groups in Lean. ~ Antoine Chambert-Loir. #ITP #LeanProver #Math
• Simple groups in Lean (Video). ~ Antoine Chambert-Loir. #ITP #LeanProver #Math
• Metaprogramming in Lean, Talk 1 (June 23, 2025). ~ Heather Macbeth. #ITP #LeanProver
• Metaprogramming in Lean, Talk 2 (June 24, 2025). ~ Heather Macbeth. #ITP #LeanProver
• Metaprogramming in Lean, Talk 3 (June 25, 2025). ~ Heather Macbeth. #ITP #LeanProver
• The Lean FRO year 3 roadmap. #ITP #LeanProver