Las lecturas compartidas en Mastodon el 2 de agosto de 2024 son

• Lecturas compartidas el 1 de agosto de 2024. #ITP #Lean4 #Mathlib #Coq #Math #Haskell #FunctionalProgramming
• Semialgebraic groups and generalized affine buildings. ~ Raphael Appenzeller. #PhDThesis #ITP #LeanProver #Math
• Lie groups and algebras (in Isabelle/HOL). ~ Richard Schmoetten & Jacques D. Fleuriot. #ITP #IsabelleHOL #Math
• Semantical analysis of intuitionistic modal logics between CK and IK. ~ Jim de Groot, Ian Shillito & Ranald Clouston. #ITP #Coq #Logic
• Computer-assisted proofs for Lyapunov stability via sums of squares certificates and constructive analysis. ~ Grigory Devadze, Victor Magron & Stefan Streif. #ITP #MinLog #Math
• A framework for semiring-annotated type systems. ~ James Wood. #ITP #Agda #TypeTheory
• Where does the name "algebraic data type" come from? ~ Li-yao Xia (@lysxia). #FunctionalProgramming #Hope #Miranda
• Analyzing Haskell stability. ~ Jappie Klooster (@jappieklooster). #Haskell #FunctionalProgramming
• Data.Maybe, and thoughts on library design. ~ Srijan Paul (@_injuly). #Haskell #FunctionalProgramming
• Esta vez sí: Con la IA, nada será igual en la Universidad. ~ Mariano Fernández Enguita. #IA #Educación
• La demanda de educación superior ante el cambio tecnológico y la inteligencia artificial. ~ José Ignacio Conde-Ruiz, Juan José Ganuza, Manu García y Carlos Victoria. #IA #Educación
• Inteligencia Artificial y capital humano: ¿Pueden estar en peligro sus complementariedades? ~ Juan F. Jimeno y Ana Lamo. #IA

Las lecturas compartidas en Mastodon el 1 de agosto de 2024 son

• Lecturas compartidas el 31 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Logic #Math #LLMs #ATP #Reasoning
• Continuous functions — formalized in Lean4. ~ Dominic Plein & Felix Lentze. #ITP #Lean4 #Math
• Continuous functions — formalized in Lean4 (code and a LaTeX document). ~ Dominic Plein & Felix Lentze. #ITP #Lean4 #Math
• LeanSearch: Find theorems in Mathlib4 using natural language query. #ITP #Lean4 #Mathlib
• Search Mathlib: A webpage that searches for Mathlib theorems. ~ Deming Xu. #ITP #Lean4 #Mathlib
• Set Theory Game (An introduction to mathematical proof). ~ Daniel J. Velleman./#/g/djvelleman/stg4 #ITP #Lean4 #Math
• Lean Game Server (A repository of learning games for the proof assistant Lean (Lean 4) and its mathematical library Mathlib). #ITP #Lean4 #Math
• A verified foreign function interface between Coq and C. ~ Joomy Korkut, Kathrin Stark, Andrew W. Appel. #ITP #Coq
• The Haskell Unfolder Episode 30: runST. ~ Edsko de Vries (@EdskoDeVries), Andres Löh (@kosmikus@functional.cafe). #Haskell #FunctionalProgramming

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

• Lecturas compartidas el 30 de julio de 2024. #ITP #IsabelleHOL #Math #LogicProgramming #ASP #AI #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Asociatividad de la concatenación de listas". #ITP #Lean4 #IsabelleHOL #Math
• A formalization and proof checker for Isabelle’s metalogic. ~ Simon Roßkopf, Tobias Nipkow. #ITP #IsabelleHOL
• From Schütte’s formal systems to modern automated deduction. ~ Wolfgang Bibel, Jens Otten. #ATP #Logic
• Steamroller problems: An evaluation of LLM reasoning capability with automated theorem prover strategies. ~ Lachlan McGinness, Peter Baumgartner. #LLMs #ATP #Reasoning

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

• Lecturas compartidas el 29 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Math #AI #CAS
• A construction of the Lie algebra of a Lie group in Isabelle/HOL. ~ Richard Schmoetten, Jacques D. Fleuriot. #ITP #IsabelleHOL #Math
• LLASP: Fine-tuning Large Language Models for Answer Set Programming. ~ Erica Coppolillo, Francesco Calimeri, Giuseppe Manco, Simona Perri, Francesco Ricca. #AI #LLMs #LogicProgramming #ASP
• AlphaProof, AlphaGeometry, ChatGPT, and why the future of AI is neurosymbolic. ~ Gary Marcus (@garymarcus@sigmoid.social). #AI
• CalcGPT, la calculadora inútil pero «inteligente». ~ @Alvy. #ChatGPT #Math

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

• Lecturas compartidas el 28 de julio de 2024. #ITP #LeanProver #Math
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "length (replicate n x) = n". #ITP #Lean4 #IsabelleHOL #Math
• Advancing mathematics through computers and AI: Automation, discovery, and collaboration. ~Douglas C. Youvan. #AI #ITP #CAS #Math

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

• Lecturas compartidas el 27 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Math #FunctionalProgramming #Haskell
• Formalisation of the finite simple Conway groups in Lean. ~ Erik van der Plas. #ITP #LeanProver #Math
• The first Janko group J1: simplicity and formalization. ~ Roxy van de Kuilen. #ITP #LeanProver #Math

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

• Lecturas compartidas el 26 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Math #IMO #AI #AlphaProof #FunctionalProgramming #Haskell
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si u es una sucesión no decreciente y su límite es a, entonces u(n) ≤ a para todo n". #ITP #Lean4 #IsabelleHOL #Math
• Haskell nuggets: k-means. ~ Justin Lê (@mstk). #FunctionalProgramming #Haskell
• Prove or disprove. 100 conjectures from the OEIS. ~ Ralf Stephan. #Math

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

• Lecturas compartidas el 25 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Coq #Math #LLMs
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Las sucesiones divergentes positivas no tienen límites finitos". #ITP #Lean4 #IsabelleHOL #Math
• AI achieves silver-medal standard solving International Mathematical Olympiad problems. #AI #Math #IMO #Lean4 #AlphaProof #AlphaGeometry2
• Google DeepMind IMO 2024 Solutions. #AI #Math #IMO #Lean4 #AlphaProof #AlphaGeometry2
• Move over, mathematicians, here comes AlphaProof (A.I. is getting good at math — and might soon make a worthy collaborator for humans). ~ Siobhan Roberts. #AI #Math #IMO #Lean4 #AlphaProof
• To formalized mathematics and back with the Lean theorem prover. ~ Kyle Miller. #ITP #LeanProver #Math
• The mysteries and frustrations of numerical proofs. ~ Lawrence Paulson (@LawrPaulson@mathstodon.xyz). #ITP #IsabelleHOL #Math
• Formal verification of 2-3 trees in Coq. ~ Horia-Matei Cornea. #ITP #Coq
• Rivers: eventually constant streams in Haskell. ~ Brent Yorgey (@byorgey@mathstodon.xyz). #FunctionalProgramming #Haskell
• Types as interfaces. #FunctionalProgramming #Haskell

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

• Lecturas compartidas el 24 de julio de 2024. #ITP #Lean4 #Coq #Logic #FunctionalProgramming #Haskell
• #Calculemus: Demostraciones con Lean4 e Isabelle/HOL de "Si a es un punto de acumulación de la sucesión de Cauchy u, entonces a es el límite de u". #ITP #Lean4 #IsabelleHOL #Math
• Approximate relational reasoning for higher-order probabilistic programs. ~ Philipp G. Haselwarter, Kwing Hei Li, Alejandro Aguirre, Simon Oddershede Gregersen, Joseph Tassarotti, Lars Birkedal. #ITP #Coq
• LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover. ~ Zijian Wu, Jiayu Wang, Dahua Lin, Kai Chen. #LLMs #ITP #Lean4 #Math

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

• Lecturas compartidas el 23 de julio de 2024. #ITP #Lean4 #Math #FunctionalProgramming #OCaml
• Lean For Haskell developers. ~ Solomon. #ITP #Lean4 #FunctionalProgramming #Haskell
• A logic for veracity: Development and implementation. ~ Daniel Britten, Steve Reeves. #ITP #Coq #Logic
• Typed compositional quantum computation with lenses. ~ Jacques Garrigue, Takafumi Saikawa. #ITP #Coq