The readings shared in Bluesky on 27 February 2025 are

• Compactness theorem for first-order logic (in Isabelle/HOL). ~ Sophie Tourret, Lawrence C. Paulson. #ITP #IsabelleHOL #Logic #Math
• CuDIP: Enhancing theorem proving in LLMs via curriculum learning-based direct preference optimization. ~ Shuming Shi et als. #AI #LLMs #ATP #Logic #Math
• TheoremExplainAgent: Towards multimodal explanations for LLM theorem understanding. ~ Max Ku et als. #AI #LLMs #ATP #Logic #Math
• ChatGPT vs. DeepSeek: A comparative study on AI-based code generation. ~ Md Motaleb Hossen Manik. #AI #LLMs #Programming

The readings shared in Bluesky on 26 February 2025 are

• Big-Math: A large-scale, high-quality math dataset for reinforcement learning in language models. ~ Alon Albalak et als. #LLMs #Math
• UGMathBench: A diverse and dynamic benchmark for undergraduate-level mathematical reasoning with large language models. ~ Xin Xu et als. #LLMs #Math
• Empowering LLMs with logical reasoning: A comprehensive survey. ~ Fengxiang Cheng et als. #LLMs #Math #Reasoning

The readings shared in Bluesky on 25 February 2025 are

• Towards a formalized theory of solid modules. ~ Dagur Asgeirsson. #PhDThesis #ITP #LeanProver #Math
• Prove your colorings: Formal verification of cache coloring of Bao hypervisor. ~ Axel Ferréol, Laurent Corbin, Nikolai Kosmatov. #ITP #Coq #Rocq
• Logic.py: Bridging the gap between LLMs and constraint solvers. ~ Pascal Kesseli, Peter O'Hearn, Ricardo Silveira Cabral. #LLMs #Logic #SAT #SMT

The readings shared in Bluesky on 24 February 2025 are

• Formalising Brauer group and group cohomology in Lean4.~ Jujian Zhang. #ITP #LeanProver #Math
• The Haskell road to logic, math and programming. ~ Kees Doets, Jan van Eijck (2004). #Haskell #FunctionalProgramming #Logic #Math
• Bind and traverse with Kleisli morphisms. ~ Murat Kasimov. #CategoryTheory #Haskell #FunctionalProgramming
• Elements of Clojure. ~ Zachary Tellman. #Clojure #Lisp #FunctionalProgramming
• Open Reasoning Data (1,748,344 questions and 300,119 chain-of-thought traces to train open models). #AI #LLMs
• Material abierto para construir modelos de razonamiento general: 1.600.000 preguntas y 270.000 trazas de cadenas de pensamiento. ~ Por @Alvy. #AI #LLMs

The readings shared in Bluesky on 23 February 2025 are

• Power operator for lists (in Isabelle/HOL). ~ Štěpán Holub, Martin Raška, Štěpán Starosta, Tobias Nipkow. #ITP #IsabelleHOL
• Strands Rocq: Why is a security protocol correct, mechanically? ~ Matteo Busi, Riccardo Focardi, Flaminia L. Luccio. #ITP #Rocq #Coq
• Fracterm calculus for partial meadows. ~ Jan A. Bergstra, Alban Ponse. #ATP #Prover9 #Mace4 #Math
• How to deepen your understanding of Mizar. ~ Alex Nelson. #ITP #Mizar

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