The readings shared in Bluesky on 28 January 2025 are

• Readings shared January 26, 2025. #ITP #LeanProver #HOL_Light #Math
• The directed Van Kampen Theorem in Lean. ~ Henning Basoldm, Peter Bruin, Dominique Lawson. #ITP #LeanProver #Math
• The simplicity of Prolog. ~ Ties Westendorp. #Prolog #LogicProgramming
• Beautiful Racket (An introduction to language-oriented programming using Racket). ~ Matthew Butterick. #Racket #FunctionalProgramming
• New game posted on Lean Game Server: Reasoning. ~ Jad Abou Hawili./#/g/jadabouhawili/knightsandknaves-lean4game #ITP #LeanProver
• Lean for scientists and engineers. ~ Tyler Josephson. #ITP #LeanProver
• lean-mine: A collection of problems solved in Lean. #ITP #LeanProver #Math
• Baby Rudin project: An attempt to formalize every problem in Baby Rudin with natural language description. #ITP #LeanProver #Math
• Homo ratiocinator (Reckoning human). ~ Moshe Vardi. #Logic #Math