Las lecturas compartidas en Mastodon el 30 de mayo de 2024 son

• Lecturas compartidas el 29 de mayo de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell #Python
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si x, y ∈ ℝ tales que (∀ z)[y < z → x ≤ z], entonces x ≤ y". #ITP #Lean4 #IsabelleHOL #Math
• Formalising the local compactness of the adele ring. ~ Salvatore Mercuri. #ITP #Lean4 #Math
• Formalization of asymptotic convergence for stationary iterative methods. ~ Mohit Tekriwal, Joshua Miller, Jean-Baptiste Jeannin. #ITP #Coq #Math
• Certification of tail recursive bubble–sort in Theorema and Coq. ~ Isabela Dramnesc, Tudor Jebelean, and Sorin Stratulat. #ITP #Coq #Theorema
• Translating HOL-Light proofs to Coq. ~ Frédéric Blanqui. #ITP #HOL_Light #Coq
• Prover9 unleashed: Automated configuration for enhanced proof discovery. ~ Kristina Aleksandrova, Jan Jakubuv and Cezary Kaliszyk. #ATP #Prover9
• Automated theorem proving for Prolog verification. ~ Fred Mesnard, Thierry Marianne and Etienne Payet. #ATP #Vampire #TPTP #Prolog
• Free foil: Generating efficient and scope-safe abstract syntax. ~ Nikolai Kudasov, Renata Shakirova, Egor Shalagin, Karina Tyulebaeva. #FunctionalProgramming #Haskell
• Automated theorem provers help improve large language model reasoning. ~ Lachlan McGinness and Peter Baumgartner. #LLMS #ATP