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

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

• Lecturas compartidas el 22 de julio de 2024. #AI
• Proseminar on computer-assisted mathematics, session 7: Introduction to Lean. ~ Judith Ludwig, Florent Schaffhauser. #ITP #Lean4 #Math
• Proseminar on computer-assisted mathematics, session 7: Introduction to Lean (Code). ~ Judith Ludwig, Florent Schaffhauser. #ITP #Lean4 #Math
• (Pro)Seminar on computer-assisted mathematics. ~ Judith Ludwig, Florent Schaffhauser. #CAS #Sage #ITP #LeanProver #Math
• Practical deductive verification of OCaml programs (Extended version). ~ Mário Pereira. #FunctionalProgramming #OCaml

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

• Lecturas compartidas el 21 de julio de 2024. #ITP #IsabelleHOL #Coq #Logic #Math #FunctionalProgramming #Haskell #LiquidHaskell
• Un robot que resuelve rompecabezas 200 veces más rápido que las personas más hábiles. ~ @Alvy. #AI

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

• Lecturas compartidas el 20 de julio de 2024. #ITP #Lean4 #IsabelleHOL #Coq #FunctionalProgramming #Haskell #Logic #CompSci
• A gentle introduction to Isabelle and Isabelle/HOL. ~ Gunnar Teege. #ITP #IsabelleHOL
• A tree rewriting system for the Reflection Calculus. ~ Sofía Santiago-Fernández, Joost J. Joosten, David Fernández-Duque. #ITP #Coq #Logic
• Automated proof tactics for model transformation. ~ Julien Cohen, Massimo Tisi, Remi Douence. #ITP #Coq
• Liquid amortization: Proving amortized complexity with LiquidHaskell (Functional pearl). ~ Jan van Brügge. #FunctionalProgramming #Haskell #LiquidHaskell
• Monumental proof settles geometric Langlands conjecture. ~ Erica Klarreich (@EricaKlarreich). #Math