The readings shared in Bluesky on 23 May 2025 are

• A formal proof of complexity bounds on diophantine equations. ~ Jonas Bayer, Marco David. #ITP #IsabelleHOL #Math
• Solving guarded domain equations in presheaves over ordinals and mechanizing it. ~ Sergei Stepanenko, Amin Timany. #ITP #RocqProver #CategoryTheory
• Ineq-Comp: Benchmarking human-intuitive compositional reasoning in automated theorem proving on inequalities. ~ Haoyu Zhao et als. #LLMs #ITP #LeanProver #Math
• CLEVER: A curated benchmark for formally verified code generation. ~ Amitayush Thakur et als. #LLMs #ITP #LeanProver #AIforCode
• Formalisation of fairness notions in assignment problem. ~ Duc Minh Do. #ITP #IsabelleHOL