Las lecturas compartidas en Mastodon el 5 de julio de 2024 son

• Lecturas compartidas el 4 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell #Python #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las familias de conjuntos definen relaciones simétricas". #ITP #Lean4 #IsabelleHOL #Math
• Automated reasoning for mathematics. ~ Jeremy Avigad. #ATP #ITP #Math
• Fast and verified UNSAT certificate checking. ~ Peter Lammich. #ITP #IsabelleHOL #SAT
• Formalizing chemical physics using the Lean theorem prover. ~ Maxwell P. Bobbin, Samiha Sharlin, Parivash Feyzishendi, An Hong Dang, Catherine M. Wraback, Tyler R. Josephson. #ITP #Lean4
• Formalising Fermat’s last theorem for exponent 3 in Lean. ~ Pietro Monticone. #ITP #Lean4 #Math
• Verificació formal de formes equivalents de l’axioma d’elecció. ~ Vicent Pons Llopis. #TFG #ITP #Lean4 #Math
• An empirical assessment of progress in automated theorem proving. ~ Geoff Sutcliffe et als. #ATP
• Lemma discovery and strategies for automated induction. ~ Sólrún Halla Einarsdóttir, Márton Hajdu, Moa Johansson, Nicholas Smallbone, Martin Suda. #FunctionalProgramming #Haskell
• A technological approach to teaching inequalities, propositional and predicate logic. ~ Zoltán Kovács, Reinhard Oldenburg. #Logic #GeoGebra
• A natural-language proof assistant for higher-order logic (Work in progress). ~ Adam Dingle. #ITP #Natty #OCaml
• Natty: a natural-language proof assistant with an embedded automatic prover for higher-order logic. ~ Adam Dingle. #ITP #Natty #OCaml
• Learning formal mathematics from intrinsic motivation. ~ Gabriel Poesia, David Broman, Nick Haber, Noah D. Goodman. #Math #AI
• The sad state of property-based testing libraries. ~ #FunctionalProgramming #Haskell