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