The readings shared in Bluesky on 22 February 2025 are

• Lambda calculus and Lisp, part 1. #LambdaCalculus #Lisp
• Lambda calculus and Lisp, part 2. #LambdaCalculus #Emacs #Lisp

The readings shared in Bluesky on 21 February 2025 are

• Machine-assisted proofs (February 19, 2025). ~ Terence Tao. #ITP #LeanProver #AI #Math
• Formalisation of combinatorial optimisation in Isabelle/HOL: Network flows. ~ Thomas Ammer. #ITP #IsabelleHOL #Math
• A Coq implementation of a theory of tagged objects. ~ Matthew Gates, Alex Potanin. #ITP #Coq #Rocq
• Formal analysis of electrical circuit network topologies using theorem proving, ~ Kubra Aksoy, Adnan Rashid1, Osman Hasan, Sofiene Tahar. #ITP #IsabelleHOL
• Learn programming with OCaml (Algorithms and data structures). ~ Sylvain Conchon, Jean-Christophe Filliâtre. #OCaml #FunctionalProgramming
• Formalizing complex mathematical statements with LLMs: A study on mathematical definitions. ~ Lan Zhang, Marco Valentino, Andre Freitas. #LLMs #Math #Autoformalization #ITP #IsabelleHOL
• Diverse inference and verification for advanced reasoning. ~ Iddo Drori et als. #LLMs #ITP #LeanProver #Autoformalization
• Advice for writing proofs. ~ Evan Chen (2023). #Math
• Intro to proofs for the morbidly curious. ~ Evan Chen (2024). #Math

The readings shared in Bluesky on 20 February 2025 are

• Simplifying formal proof-generating models with ChatGPT and basic searching techniques. ~ Sangjun Han et als. #LLMs #ITP #LeanProver
• Proving olympiad inequalities by synergizing LLMs and symbolic reasoning. ~ Zenan Li et als. #LLMs #ITP #LeanProver #Math
• The role of GitHub Copilot on software development: A perspective on productivity, security, best practices and future directions. ~ Suresh Babu Nettur et als. #LLMs #Programming
• Competitive programming with large reasoning models. ~ OpenAI. #LLMs #Programming
• A brief introduction to olympiad inequalities. ~ Evan Chen. #Math
• Topics in inequalities: Theorems and techniques. ~ Hojoo Lee. #Math
• 567 nice and hard inequalities. ~ Nguyen Duy Tung. #Math
• #Exercitium: Lista cuadrada. #Haskell #Python #CommonLisp

The readings shared in Bluesky on 19 February 2025 are

• Automating math (Computers can already help verify proofs. One day soon, AI may be able to come up with new ones). ~ Adam Marblestone. #ITP #LeanProver #AI #LLMs #Math
• These years in Common Lisp: 2023-2024 in review. ~ Vincent Dardel. #CommonLisp
• From informal to formal - Incorporating and evaluating LLMs on natural language requirements to verifiable formal proofs. ~ Jialun Cao et als. #LLMs #Reasoning #Math #ITP #LeanProver #Coq
• ProofWala: Multilingual proof data synthesis and theorem-proving. ~ Amitayush Thakur et als. #LLMs #ITP #LeanProver #Coq
• Integrating arithmetic learning improves mathematical reasoning in smaller models. ~ Neeraj Gangwar, Suma P Bhat, Nickvash Kani. #ITP #Math #Reasoning
• Theorem prover as a judge for synthetic data generation. ~ Joshua Ong Jun Leang et als. #LLMs #ITP
• A mechanistic interpretation of syllogistic reasoning in auto-regressive language models. ~ Geonhee Kim, Marco Valentino, André Freitas. #LLMs #Logic #Reasoning
• Teaching LLMs according to their aptitude: Adaptive reasoning for mathematical problem solving. ~ Xin Xu et als. #LLMs #Math
• LLMs for mathematical modeling: Towards bridging the gap between natural and mathematical languages. ~ Xuhan Huang et als. #LLMs #Math
• Step guided reasoning: Improving mathematical reasoning using guidance generation and step reasoning. ~ Lang Cao et als. #LLMs #Reasoning #Math
• #Exercitium: Máximos locales. #Haskell #Python #CommonLisp #Math

The readings shared in Bluesky on 18 February 2025 are

• Large language models and mathematical reasoning failures. ~ Johan Boye, Birger Moell. #AI #LLMs #Math
• #Exercitium: Matrices de Toepliz. #Haskell #Python #CommonLisp #Math

The readings shared in Bluesky on 17 February 2025 are

• Natural transformations as a basis of control. ~ Murat Kasimov. #Haskell #FunctionalProgramming
• To type or not to type? ~ Jonathan Chun. #Python #Programming
• Diverse inference and verification for advanced reasoning. ~ Iddo Drori et als. #AI #LLMs #ITP #LeanProver
• MathConstruct: Challenging LLM reasoning with constructive proofs. ~ Mislav Balunović et als. #AI #LLMs #Math
• MathGAP: Out-of-distribution evaluation on problems with arbitrarily complex proofs. ~ Andreas Opedal et als. #AI #LLMs #Math
• Personalizando Emacs. ~ Ivan Agosto. #Emacs

The readings shared in Bluesky on 16 February 2025 are

• The relationship between category theory, lambda calculus, and functional programming in Haskell. ~ Antonio Montano. #Haskell #FunctionalProgramming #CategoryTheory #LambdaCalculus
• Logical reasoning in large language models: A survey. ~ Hanmeng Liu et als. #LLMs #Logic #Reasoning

The readings shared in Bluesky on 15 February 2025 are

• Prospects for formalizing the theory of weak infinite-dimensional categories. ~ Emily Riehl. #ITP #LeanProver #Math

The readings shared in Bluesky on 14 February 2025 are

• Language models for verifiable mathematical automation (Interaction, integration, and autoformalization). ~ Qiaochu Jiang. #ITP #IsabelleHOL #LLMs #Autoformalization
• The Haskell Unfolder Episode 39: Deriving strategies). ~ Edsko de Vries, Andres Löh. #Haskell #FunctionalProgramming
• #Exercitium: Primos equidistantes. #Haskell #Python #CommonLisp

The readings shared in Bluesky on 13 February 2025 are

• A Coq formalization of unification modulo exclusive-or. ~ Yichi Xu, Daniel J. Dougherty, Rose Bohrer. #ITP #Coq
• Logical relations for formally verified authenticated data structures. ~ Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti. #ITP #Coq #Rocq
• A proof of Hilbert basis theorem and an extension to formal power series (in Isabelle/HOL). ~ Benjamin Puyobro, Benoît Ballenghien, Burkhart Wolff. #ITP #IsabelleHOL #Math
• Why Amazon is betting on 'automated reasoning' to reduce AI's hallucinations. ~ Belle Lin. #AI #LLMs #ITP
• On LLM-generated logic programs and their inference execution methods. ~ Paul Tarau. #LLMs #LogicProgramming #Prolog
• LP-LM: No hallucinations in question answering with logic programming. ~ Katherine Wu, Yanhong A. Liu. #LLMs #LogicProgramming #Prolog
• Improving autoformalization using type checking. ~ Auguste Poiroux, Gail Weiss, Viktor Kunčak, Antoine Bosselut. #Autoformalization #LLMs #ITP #LeanProver #Math
• What makes math problems hard for reinforcement learning: a case study. ~ Ali Shehper et als. #LLMs #Math
• A model for learning-curve estimation in efficient neural architecture search and its application in predictive health maintenance. ~ David Solís-Martín, Juan Galán-Páez, Joaquín Borrego-Díaz. #AI
• 50 years of programming language evolution through the software Heritage looking glass. ~ Adèle Desmazières, Roberto Di Cosmo, Valentin Lorentz. #Programming