The readings shared in Bluesky on 10 March 2025 are

• The burden of proof: Automated tooling for rapid iteration on large mechanised proofs. ~ Chengsong Tan, Alastair F. Donaldson, Jonathan Julián Huerta y Munive, John Wickerson. #ITP #IsabelleHOL
• MiniF2F in Rocq: Automatic translation between proof assistants (a case study). ~ Jules Viennot, Guillaume Baudart, Emilio Jesúss Gallego Arias, Marc Lelarge. #LLMs #Rocq #LeanProver #IsabelleHOL #Math
• Generating millions of Lean theorems with proofs by exploring state transition graphs. ~ David Yin, Jing Gao. #LLMs #LeanProver #Math
• New proofs expand the limits of what cannot be known (By proving a broader version of Hilbert’s famous 10th problem, two groups of mathematicians have expanded the realm of mathematical unknowability). ~ Joseph Howlett. #Math
• Les sept problèmes mathématiques du prix du millénaire. ~ Nicolas Bacaër et als. #Math
• How to get a Common Lisp job in 2055. ~ Sebastian Carlos. #CommonLisp
• #Exercitium: Iguales al siguiente. #Haskell
• #Calculemus: Celebración del día mundial de la lógica. #IsabelleHOL #Lógica #Matemática
• Curso "Programación declarativa (2003-04)" #LogicProgramming #Prolog