The readings shared in Bluesky on 9 March 2025 are

• Floating point numbers in Lean. ~ Joseph McKinsey. #ITP #LeanProver #Math
• Flean: Floating point numbers in Lean, mostly done! ~ Joseph McKinsey. #ITP #LeanProver #Math
• Curso "Lógica informática" (2003-04). #Logic #Math #CompSci

The readings shared in Bluesky on 8 March 2025 are

• Sum types and subtypes and unions. ~ Justin Le. #Haskell #FunctionalProgramming

The readings shared in Bluesky on 7 March 2025 are

• A formalisation of addition chains. ~ Laurent Théry. #ITP #Coq #Rocq
• QED in context (An observation study of proof assistant users). ~ Jessica Shi, Cassia Torczon, Harrison Goldstein, Benjamin C. Pierce, Andrew Head #ITP #LeanProver #Coq #Rocq
• On the formalization of the simplicial model of HoTT. ~ Kunhong Du. #ITP #Agda #HoTT
• A gentle introduction to categorical logic and type theory. ~ Eric Schmid. #Math #CategoryTheory #TypeTheory
• MathMistake checker: A comprehensive demonstration for step-by-step math problem mistake finding by prompt-guided LLMs. ~ Tianyang Zhang et als. #LLMs #Math
• A survey on Large Language Models for code generation. ~ Nam Huynh, Beiyu Lin. #LLMs #Programming
• Markov chain of thought for efficient mathematical reasoning. ~ Wen Yang, Minpeng Liao, Kai Fan. #LLMs #Math #Reasoning
• Assisting mathematical formalization with a learning-based premise retriever. ~ Yicheng Tao et als. #LLMs #ITP #LeanProver

The readings shared in Bluesky on 6 March 2025 are

• Cryptis: Cryptographic reasoning in separation logic. ~ Arthur Azevedo de Amorim, Amal Ahmed, Marco Gaboardi. #ITP #Coq #Rocq
• Lean-STaR: Learning to interleave thinking and proving. ~ Haohan Lin et als. #LLMs #ITP #LeanProver
• MA-LoT: Multi-agent lean-based long chain-of-thought reasoning enhances formal theorem proving. ~ Ruida Wang et als. #LLMs #ITP #LeanProver
• FANS: Formal answer selection for natural language math reasoning using Lean4. ~ Jiarui Yao, Ruida Wang, Tong Zhang. #LLMs #ITP #LeanProver
• From informal to formal (Incorporating and evaluating LLMs on natural language requirements to verifiable formal proofs). ~ Jialun Cao et als. #LLMs #ITP #LeanProver

The readings shared in Bluesky on 5 March 2025 are

• Language partitioning for mission-time linear temporal logic (in Isabelle/HOL). ~ Zili Wang, Katherine Kosaian, Alec Rosentrater. #ITP #IsabelleHOL
• Unos profesores avisan de que la IA supone una amenaza para el pensamiento crítico de los estudiantes: "escribir también es pensar". ~ Marcos Merino. #AI #Education

The readings shared in Bluesky on 4 March 2025 are

• Formalizing zeta and L-functions in Lean. ~ David Loeffler, Michael Stoll. #ITP #LeanProver #Math
• Lean Copilot: Large language models as copilots for theorem proving in Lean. ~ Peiyang Song, Kaiyu Yang, Anima Anandkumar. #LLMs #ITP #LeanProver
• Gold-medalist performance in solving olympiad geometry with AlphaGeometry2. ~ Yuri Chervonyi et als. #AI #AlphaGeometry #Math
• NL2FOL: Translating natural language to first-order logic for logical fallacy detection. ~ Abhinav Lalwani et als. #LLMs #Logig #SMT
• Utilizing ChatGPT in a data structures and algorithms course: A teaching assistant's perspective. ~ Pooriya Jamie, Reyhaneh Hajihashemi, Sharareh Alipour. #LLMs #CompSci
• Performance review on LLM for solving Leetcode problems. ~ Lun Wang et als. #LLMs #Programming
• InductionBench: LLMs fail in the simplest complexity class. ~ Wenyue Hua et als. #LLMs #Reasoning

The readings shared in Bluesky on 2 March 2025 are

• Faithful logic embeddings in HOL (A recipe to have it all: deep and shallow, automated and interactive, heavy and light, proofs and counterexamples, meta and object level). ~ Christoph Benzmüller. #ITP #IsabelleHOL
• BiCoq: Bigraphs formalisation with Coq. ~ Cécile Marcon et als. #ITP #Coq #Rocq

The readings shared in Bluesky on 2 March 2025 are

• Waterproof: Transforming a proof assistant into an educational tool. ~ Aalt Jelle Wemmenhove. #ITP #Coq #Math #Education
• Computer assisted mathematical proofs: using the computer to verify computers. ~ Herman Geuvers. #ITP #Math
• An invitation to Blueprint-driven formalisation of mathematical research in Lean. ~ Pietro Monticone. #ITP #LeanProver #Math
• An invitation to Blueprint-driven formalisation of mathematical research in Lean (Codes). ~ Pietro Monticone. #ITP #LeanProver #Math
• Formalizing MLTL formula progression in Isabelle/HOL. ~ Katherine Kosaian, Zili Wang, Elizabeth Sloan, Kristin Rozier. #ITP #IsabelleHOL #Logic
• Applying purity to the imperative world. ~ Jeremy Bowers. #Haskell #FunctionalProgramming
• ¿Podemos creer la prueba de la conjetura? ~ Marta Macho Stadler. #Math #CompSci

The readings shared in Bluesky on 1 March 2025 are

• Functional pearl: How much is in a square? Calculating functional programs with squares. ~ Jose Nuno Oliveira. #FunctionalProgramming #Haskell
• A combinatorial identities benchmark for theorem proving via automated theorem generation. ~ Beibei Xiong et als. #LLMs #ITP #LeanProver #Math
• Herald: A natural language annotated Lean 4 dataset. ~ Guoxiong Gao et als. #LLMs #ITP #LeanProver #Math
• LeanProgress: Guiding search for neural theorem proving via proof progress prediction. ~ Suozhi Huang et als. #LLMs #ITP #LeanProver

The readings shared in Bluesky on 28 February 2025 are

• Is mathematics obsolete? ~ Jeremy Avigad. #Math #ITP #LeanProver #AI #LLMs
• Faithful logic embeddings in HOL (A recipe to have it all: deep and shallow, automated and interactive, heavy and light, proofs and counterexamples, meta and object level). ~ Christoph Benzmüller. #ITP #IsabelleHOL #Logic
• Mathematical introduction to deep learning: Methods, implementations, and theory. ~ Arnulf Jentzen, Benno Kuckuck, Philippe von Wurstemberger. #AI #DeepLearning #Math
• Teaching LLMs according to their aptitude: Adaptive reasoning for mathematical problem solving. ~ Xin Xu et als. #AI #LLMs #Math
• Homo ratiocinator (reckoning human). ~ Moshe Y. Vardi. #Logic #CompSci
• PPA: Un asistente de demostración para lógica de primer orden con extracción de testigos usando la traducción de Friedman. ~ Manuel Panichelli. #Haskell #FunctionalProgramming #Logic