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

• Is mathematics obsolete? ~ Jeremy Avigad. #Math #ITP #LeanProver #AI #LLMs
• 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

The readings shared in Bluesky on 12 February 2025 are

• STP: Self-play LLM theorem provers with iterative conjecturing and proving. ~ Kefan Dong, Tengyu Ma. #LLMs #ITP #LeanProver #IsabelleHOL
• Competitive programming with large reasoning models. ~ OpenAI. #LLMs #Programming

The readings shared in Bluesky on 11 February 2025 are

• Examining false positives under inference scaling for mathematical reasoning. ~ Yu Wang, Nan Yang, Liang Wang, Furu Wei. #LLMs #Math #Reasoning
• MATH-perturb: Benchmarking LLMs' math reasoning abilities against hard perturbations. ~ Kaixuan Huang et als. #LLMs #Math #Reasoning
• Embedding self-correction as an inherent ability in large language models for enhanced mathematical reasoning. ~ Kuofeng Gao, Huanqia Cai, Qingyao Shuai, Dihong Gong, Zhifeng Li. #LLMs #Math #Reasoning
• Streams in Common Lisp. ~ jcs. #CommonLisp
• Functional streams. ~ Atabey Kaygun. #CommonLisp
• Programming techniques: Generating prime numbers in Common Lisp. ~ Mitchell Chung. #CommonLisp #Math

The readings shared in Bluesky on 10 February 2025 are

• Feedback loops guide AI to proof checking. ~ Chris Edwards. #AI #ITP #LeanProver #Coq
• Verified certificates via SAT and computer algebra systems for the Ramsey R(3,8) and R(3,9) problems. ~ Zhengyu Li, Conor Duggan, Curtis Bright, Vijay Ganesh. #SAT #CAS
• Proving the coding interview: A benchmark for formally verified code generation. ~ Quinn Dougherty, Ronak Mehta. #AI #LLMs #Python #ITP
• ATLAS: Autoformalizing theorems through lifting, augmentation, and synthesis of data. ~ Xiaoyang Liu, Kangjie Bao, Jiashuo Zhang, Yunqi Liu, Yu Chen, Yuntian Liu, Yang Jiao, Tao Luo. #LLMs #ITP #LeanProver #Math #Autoformalization
• Can Transformers reason logically? A study in SAT solving. ~ Leyan Pan, Vijay Ganesh, Jacob Abernethy, Chris Esposo, Wenke Lee. #LLMs #Reasoning #SAT_Solvers
• #Exercitium: Anagramas. #Haskell #Python #CommonLisp