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