Readings shared January 22, 2025
The readings shared in Bluesky on 22 January 2025 are
- Readings shared January 21, 2025. #ITP #Lean4 #IsabelleHOL #Math #Prolog #LogicProgramming #AI #LLMs
- #Exercitium: Iguales al siguiente. #Haskell #Python #Matemáticas
- Formalising new mathematics in Isabelle: Diagonal Ramsey. ~ Lawrence C Paulson. #ITP #IsabelleHOL #Math
- Logical relations for formally verified authenticated data structures. ~ Simon Oddershede Gregersen, Chaitanya Agarwal, Joseph Tassarotti. #ITP #Coq #Rocq
- Advent of Code 2024: Haskell solution reflections for all 25 days. ~ Justin Le. #Haskell #FunctionalProgramming
- Scientific computing in Lean. ~ Tomas Skrivan. #ITP #LeanProver #Math
- Alpha-beta pruning explored, extended and verified. ~ Tobias Nipkow. #ITP #IsabelleHOL
- Can a computer judge interestingness? ~ Michael Douglas. #AI #Math
- Formalising real algebraic geometry. ~ Artie Khovanov, Michael Nedzelsky, Wenda Li. #ITP #IsabelleHOL #Math
- The Mandelbrot set is connected (and other Lean explorations). ~ Geoffrey Irving. #ITP #LeanProver #Math
- Formalising theory of combinatorial optimisation. ~ Mohammad Abdulaziz. #ITP #IsabelleHOL #Math
- Condensed type theory. ~ Johan Commelin. #ITP #LeanProver #Math
- How to prove Fermat's Last Theorem. ~ Kevin Buzzard. #ITP #LeanProver #Math
- Structures in dependent type theory. ~ Jeremy Avigad. #ITP #LeanProver
- Comparative formalisation of Kneser's theorem. ~ Mantas Bakšys, Yaël Dillies. #ITP #IsabelleHOL #LeanProver #Math
- Lawvere theories in Lean. ~ Adam Topaz. #ITP #LeanProver #Math
- How to teach Fourier analysis to a large library of formalised mathematics. ~ Yaël Dillies. #ITP #LeanProver #Math
- Computer algebra and the formalisation of new mathematics. ~ Lawrence Paulson. #ITP #IsabelleHOL #Math
- Formalizing the divided power envelope in Lean. ~ María Inés de Frutos Fernández. #ITP #LeanProver #Math
- New Foundations: the story of a large formalisation project. ~ Sky Wilshaw. #ITP #LeanProver #Math
- The mathematics of Artificial Intelligence. ~ Gabriel Peyré. #AI #Math
- The Ramanujan Library (Automated discovery on the hypergraph of integer relations). ~ Itay Beit-Halachmi, Ido Kaminer. #Math #CompSci
- Wikenigma: An encyclopedia of unknowns. #Math #CompSci