The readings shared in Bluesky on 20 February 2025 are

• Simplifying formal proof-generating models with ChatGPT and basic searching techniques. ~ Sangjun Han et als. #LLMs #ITP #LeanProver
• Proving olympiad inequalities by synergizing LLMs and symbolic reasoning. ~ Zenan Li et als. #LLMs #ITP #LeanProver #Math
• The role of GitHub Copilot on software development: A perspective on productivity, security, best practices and future directions. ~ Suresh Babu Nettur et als. #LLMs #Programming
• Competitive programming with large reasoning models. ~ OpenAI. #LLMs #Programming
• A brief introduction to olympiad inequalities. ~ Evan Chen. #Math
• Topics in inequalities: Theorems and techniques. ~ Hojoo Lee. #Math
• 567 nice and hard inequalities. ~ Nguyen Duy Tung. #Math
• #Exercitium: Lista cuadrada. #Haskell #Python #CommonLisp