The readings shared in Bluesky on 25 December 2024 are

• Readings shared December 24, 2024. #ITP #Agda #Haskell #FunctionalProgramming #Haskell #Python #AI #LLMs #Math
• #Exercitium: El teorema de Navidad de Fermat. #Haskell #Python #Math
• Lean: First steps (20 - Contradictory cases). ~ Tariq Rashid. #ITP #LeanProver #Lean4 #Math
• The bipolar Lisp programmer. ~ Mark Tarver. #Lisp #Programming

The readings shared in Bluesky on 24 December 2024 are

• Readings shared December 23, 2024. #AI #Math #Reasoning #ITP #Coq #IsabelleHOL #LeanProver #Autoformalization #Programming #JuliaLang #Python #MachineLearning #Golog #LogicProgramming
• #Exercitium: Producto de los elementos de la diagonal principal. #Haskell #Python #Matemáticas
• Teaching and learning proof in mathematics at university: new perspectives in education with proof assistants? ~ Cécile Ouvrier-Buffet. #ITP #Math #Education
• Data for mathematical copilots: Better ways of presenting proofs for machine learning. ~ Simon Frieder et als. #AI #LLMs #Math
• Compiling dependent type preconditions to runtime checks with Agda2Hs. ~ Jakob Naucke. #ITP #Agda #Haskell #FunctionalProgramming

The readings shared in Bluesky on 23 December 2024 are

• Readings shared December 21, 2024. #ITP #IsabelleHOL #Math #Haskell #FunctionalProgramming
• Formal mathematical reasoning: A new frontier in AI. ~ Kaiyu Yang, Gabriel Poesia, Jingxuan He, Wenda Li, Kristin Lauter, Swarat Chaudhuri, Dawn Song. #AI #Math #Reasoning #ITP #Coq #IsabelleHOL #LeanProver #Autoformalization
• Can AI do maths yet? Thoughts from a mathematician. ~ Kevin Buzzard. #AI #ITP #Math
• The state of Julia for scientific machine learning. ~ Edward Berman, Jacob Ginesin. #Programming #JuliaLang #Python #MachineLearning
• LTLf synthesis on first-order agent programs in nondeterministic environments. ~ Till Hofmann, Jens Claßen. #AI #Golog #LogicProgramming

The readings shared in Bluesky on 21 December 2024 are

• Readings shared December 20, 2024. #ITP #Mizar #Math #Haskell #Python #AI
• Isabelle quick start guide. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
• An imperative programmer tries to learn Haskell. ~ Thane Thomson. #Haskell #FunctionalProgramming
• Solving perfect numbers quickly with Haskell. ~ Andrew MacGillivray. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 20 December 2024 are

• Readings shared December 19, 2024. #ITP #IsabelleHOL #Mizar #Logic #Math #Haskell #FunctionalProgramming #LLMs
• #Exercitium: Reiteración de suma de consecutivos. #Haskell #Python #Matemáticas
• Formalize the octonions. ~ Alex Nelson (‪@pqnelson.bsky.social‬). #ITP #Mizar #Math
• Apriori knowledge in an era of computational opacity: The role of AI in mathematical discovery. ~ Eamon Duede, Kevin Davey. #AI #Math

The readings shared in Bluesky on 19 December 2024 are

• Readings shared December 18, 2024. #ITP #Agda #Mizar #Math #AI
• A formalization of sequent calculus for classical implicational logic. ~ Frederik Krogsdal Jacobsen, Jørgen Villadsen. #ITP #IsabelleHOL #Logic
• Elementary number theory problems (Part XV – Diophantine equations). ~ Karol Pąk, Artur Korniłowicz. #ITP #Mizar #Math
• Linear calculi: A comparison approach. ~ Ana Jorge Carvalho de Soares Almeida. #Haskell #FunctionalProgramming
• A survey of mathematical reasoning in the era of multimodal large language model: Benchmark, method & challenges. ~ Yibo Yan et als. #LLMs #Math #Reasoning

The readings shared in Bluesky on 18 December 2024 are

• Readings shared December 16, 2024. #ITP #LeanLang #Lean4 #Logic #SMT #Z3 # #Haskell #FunctionalProgramming #CommonLisp #Programming #AI #Math
• Intrinsic verification of parsers and formal grammar theory in dependent Lambek calculus. ~ Steven Schaefer et als. #ITP #Agda
• Proofs in the Wild. ~ Mike Dodds. #ITP #AI
• Loops in Mizar. ~ Alex Nelson (‪@pqnelson.bsky.social‬). #ITP #Mizar #Math
• Artificial intelligence: Principles and practice. ~ George F. Luger. #AI

The readings shared in Bluesky on 16 December 2024 are

• Readings shared December 15, 2024. #Haskell #FunctionalProgramming #CategoryTheory #AI #ITP #LeanProver #Math
• Lean: First steps (19 - Reductio ad absurdum). ~ Tariq Rashid. #ITP #LeanLang #Lean4 #Math
• Bottom-up computation using trees of sublists. ~ Shin-Cheng Mu. #Haskell #FunctionalProgramming
• 'Lean-style' tactics in Knuckledragger. ~ Philip Zucker. #Logic #SMT #Z3 #Python
• An example of goal-directed, calculational proof. ~ Roland Carl Backhouse, Walter Guttmann, Michael Winter. #Logic
• Pascal Costanza's Highly Opinionated Guide to Lisp. ~ Pascal Costanza. #CommonLisp #Programming
• Proposing and solving olympiad geometry with guided tree search. ~ Chi Zhang et als. #AI #Math

The readings shared in Bluesky on 15 December 2024 are

• Readings shared December 13, 2024. #ITP #IsabelleHOL #Coq #Rocq #ATP #Prover9 #Mace4 #Logic #Math
• Category theory using Haskell (An introduction with Moggi and Yoneda). ~ Shuichi Yukita. #Haskell #FunctionalProgramming #CategoryTheory
• The future of Math with o1 reasoning with Terence Tao, Mark Chen, and James Donovan. #AI #ITP #LeanProver #Math

The readings shared in Bluesky on 13 December 2024 are

• Readings shared December 12, 2024. #ITP #LeanLang #Lean4 #Math
• On extending incorrectness logic with backwards reasoning. ~ Freek Verbeek, Md Syadus Sefat, Zhoulai Fu, Binoy Ravindran. #ITP #IsabelleHOL
• Machine checked proofs and programs in algebraic combinatorics. ~ Florent Hivert. #ITP #Coq #Rocq #Math
• Univocity of intuitionistic and classical connectives. ~ Rodolfo C. Ertola-Biraben, Branden Fitelson. #ATP #Prover9 #Mace4 #Logic #Math