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