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