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

The readings shared in Bluesky on 9 February 2025 are

• What is a quotient? ~ Kevin Buzzard. #ITP #LeanProver #Math
• Systems correctness practices at AWS: Leveraging formal and semi-formal methods. ~ Marc Brooker, Ankush Desai. #FormalMethods #ITP #LeanProver
• Turner, Bird, Eratosthenes: An eternal burning thread. ~ Jeremy Gibbons. #Haskell #FunctionalProgramming
• Chatbot software begins to face fundamental limitations. ~ Anil Ananthaswamy. #LLMs

The readings shared in Bluesky on 8 February 2025 are

• Verification of the CVM algorithm with a new recursive analysis technique. ~ Emin Karayel, Derek Khu, Kuldeep S. Meel, Yong Kiam Tan, Seng Joe Watt. #ITP #IsabelleHOL
• Review of "Haskell in depth" by Vitaly Bragilevsky. ~ Brent Yorgey. #Haskell #FunctionalProgramming
• Cervantes, la cuadratura del círculo y la búsqueda del punto fijo. ~ Tomás Domínguez Benavides. #Matemáticas

The readings shared in Bluesky on 6 February 2025 are

• A formalization of Borel determinacy in Lean. ~ Sven Manthe. #ITP #LeanProver #Math
• Simplifying formal proof-generating models with ChatGPT and basic searching techniques. ~ Sangjun Han, Taeil Hur, Youngmi Hur, Kathy Sangkyung Lee, Myungyoon Lee, Hyojae Lim. #LLMs #ChatGPT #ITP #LeanProver
• Elisp cheatsheet for Python programmers. ~ Charles Choi. #Python #Emacs #Elisp
• La categoría de conjuntos abstractos. ~ Luis Turcio. #CategoryTheory
• Exercitium: Diagonales principales. #Haskell #Python #CommonLisp #Math

The readings shared in Bluesky on 5 February 2025 are

• On the cofinality property in the context of the hierarchy of decreasing Church-Rosser abstract rewriting systems. ~ Ievgen Ivanov. #ITP #IsabelleHOL
• A semantic search engine for Mathlib4. ~ Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, Bin Dong. #ITP #LeanProver #Mathlib
• Goedel-Prover: A new frontier in automated theorem proving. ~ Yong Lin et als. #LLMs #ITP #LeanProver
• New proofs probe the limits of mathematical truth. ~ Joseph Howlett. #Math

The readings shared in Bluesky on 4 February 2025 are

• Readings shared February 3, 2025. #ITP #LeanProver #IsabelleHOL #Haskell #Python #CommonLisp #Maxima #Math
• #Exercitium: Posiciones de las diagonales principales. #Haskell #Python #CommonLisp

The readings shared in Bluesky on 3 February 2025 are

• A comprehensive survey of the Lean 4 theorem prover: Architecture, applications, and advances. ~ Xichen Tang. #ITP #LeanProver
• Differential privacy (in Isabelle/HOL). ~ Tetsuya Sato, Yasuhiko Minamide. #ITP #IsabelleHOL
• Differential privacy using quasi-Borel spaces. ~ Michikazu Hirata. #ITP #IsabelleHOL
• Maxima in the browser using Embedded Common Lisp on WASM. #Maxima #CoomonLisp #Math
• #Exercitium: La bandera tricolor. #Haskell #Python #CommonLisp

The readings shared in Bluesky on 2 February 2025 are

• Transitive union-closed families (in Isabelle/HOL). ~ Angeliki Koutsoukou-Argyraki, Lawrence C. Paulson. #ITP #IsabelleHOL
• Notes on Gödel’s and Scott’s variants of the ontological argument (Isabelle/HOL dataset). ~ Christoph Benzmüller, Dana Scott. #ITP #IsabelleHOL
• DeepSeek: A breakthrough in AI for math (and everything else). ~ David H Bailey. #DeepSeek #Math
• Some lessons from the OpenAI-FrontierMath debacle. ~ 7vik. #AI #Math
• Kazimierz Kuratowski, el talento y el compromiso de un matemático de Varsovia. ~ Marta Macho Stadler. #Math

The readings shared in Bluesky on 1 February 2025 are

• The continuous functional calculus in Lean. ~ Anatole Dedecker, Jireh Loreaux. #ITP #LeanProver #Math
• Formally verifying a transformation from MLTL formulas to regular expressions. ~ Zili Wang, Katherine Kosaian, Kristin Yvonne Rozier. #ITP #IsabelleHOL
• Formally verified binary-level pointer analysis. ~ Freek Verbeek, Ali Shokri, Daniel Engel, Binoy Ravindran. #ITP #IsabelleHOL
• A formal semantics of Core Erlang. ~ Ibrahim Abdelrahman Mohamedi. #ITP #IsabelleHOL #Erlang
• Context-dependent effects in guarded interaction trees. ~ Sergei Stepanenko, Emma Nardino, Dan Frumin, Amin Timany, Lars Birkedal. #ITP #Coq
• Reasoning about weak isolation levels in separation logic. ~ Anders Alnor Mathiasen, Léon Gondelman, Léon Ducruet, Amin Timany, Lars Birkedal. #ITP #Coq
• Assisting mathematical formalization with a learning-based premise retriever. ~ Yicheng Tao, Haotian Liu, Shanwen Wang, Hongteng Xu. #AI #LLMs #ITP #LeanProver #Math
• How to recognize artificial mathematical intelligence in theorem proving. ~ Markus Pantsar. #AI #Math #ITP
• LemmaHead: RAG assisted proof generation using large language models. ~ Tianbo Yang, Mingqi Yang, Hongyi Zhao, Tianshuo Yang. #AI #LLMs #ITP #LeanProver #Math
• Instantiation-based formalization of logical reasoning tasks using language models and logical solvers. ~ Mohammad Raza, Natasa Milic-Frayling. #LLMs #Reasoning #SMT #Z3
• From informal to formal (Incorporating and evaluating LLMs on natural language requirements to verifiable formal proofs). ~ Jialun Cao et als. #AI #LLMs #ITP #Coq #LeanProver #Math

The readings shared in Bluesky on 31 January 2025 are

• Solidifying modern SMT solvers. ~ Dominik Winterer. #SMT
• The Common Lisp Cheat Sheet. ~ Ashok Khanna. #CommonLisp
• #Exercitium: Ordenación por el máximo. #Haskell #Python #CommonLisp