The readings shared in Bluesky on 14 March 2026 are:

• From SMT solvers to Lean and the future of automated reasoning. ~ Leo de Moura, Nicola Gigante. #LeanProver #ITP
• A formalization of Borel determinacy in Lean. ~ Sven Manthe. #LeanProver #ITP #Math
• Duality theory in linear optimization and its extensions - formally verified. ~ Martin Dvorak, Vladimir Kolmogorov. #LeanProver #ITP #Math
• Optimal Caverna gameplay via formal methods. ~ Stephen Diehl. #LeanProver #ITP
• A formalization of abstract rewriting in Agda. ~ Sam Arkle, Andrew Polonsky. #Agda
• Formalization of Wallis infinite product formula for π and the Wallis integral. ~ Yasushige Watase. #Mizar #ITP #Math
• Formalization of separable version of Banach–Alaoglu theorem. ~ Hiroyuki Okazaki, Takehiko Mieno. #Mizar #ITP #Math
• The evolution and societal impact of artificial intelligence in the 21st century. ~ Monica Khadgi. #AI