The readings shared in Bluesky on 19 March 2026 are:

• Aristotle: The World's most advanced formal reasoning agent. #LeanProver #ITP #Math
• Formalization of QFT (quantum field theory). ~ Michael R. Douglas, Sarah Hoback, Anna Mei, Ron Nissim. #LeanProver #ITP #Physics
• Formalizing the classical isoperimetric inequality in the two-dimensional case. ~ Miraj Samarakkody. #LeanProver #ITP #Math
• Synthetic differential geometry in Lean. ~ Riccardo Brasca, Gabriella Clemente. #LeanProver #ITP #Math
• Formal verification of axiom-free gödelian ontological argument and trinity necessity proof in Isabelle HOL. ~ Yong-Dock Kim. #IsabelleHOL #ITP
• In the mood for inference: Logic-based natural language inference with large language models. ~ Bill Noble, Rasmus Blanck, Gijs Wijnholds. #Prover9 #ATP #LLMs
• Acertijo del día: Un reto diario de lógica. #Logic