Readings shared June 28, 2026
The readings shared in Bluesky on 28 June 2026 are:
- #RetoLean4: Soluciones del reto 7 (Demostrar que la composición de funciones inyectivas es inyectiva). #LeanProver #ITP #Math
- #RetoLean4: Propuesta del reto 8 (Demostrar, con Lean 4, que una sucesión que posee infinitos términos con valor absoluto superior a 10 no puede converger a un límite cuyo valor absoluto sea menor que 5). #LeanProver #ITP #Math
- Reseña de «What it means to be a mathematician when AI does the math?». #AI4Math #LeanProver #ITP
- A weighted Turán sieve for twin primes via the Krafft geometry. ~ Fernando Portela. #LeanProver #ITP #Math
- AXLE: A cloud infrastructure for Lean 4 theorem proving utilities. ~ Jimmy Xin, Alex Schneidman, Chris Cummins, Karun Ram, Srihari Ganesh, Jannis Limperg. #LeanProver #ITP #AI4Math
- Formalization of line search methods by Lean. ~ Yiyang Zhang, Kenneth W. Shum. #LeanProver #ITP #Math
- Formalizing a many-sorted hybrid polyadic modal logic in Lean. ~ Andrei-Alexandru Oltean, Bogdan Macovei, Ioana Leuştean. #LeanProver #ITP #Logic
- Formalization of template formulas in the modal μ-calculus in Isabelle/HOL. ~ Lise Arendsen. #IsabelleHOL #ITP #Logic
- Perron's formula (in Isabelle/HOL). ~ Manuel Eberl. #IsabelleHOL #ITP #Math
- The Dottie number. ~ Lawrence Paulson. #IsabelleHOL #ITP #Math #AI4Math
- Proving the fundamental theorem of arithmetic in Agda. ~ Brent Yorgey. #Agda #ITP #Math
- AI in mathematics is forcing big questions (What it means to be a mathematician when AI does the math?). ~ Benjamin Skuse. #AI4Math #LeanProver #ITP
- Discovering new theorems via LLMs with in-context proof learning in Lean. ~ Kazumi Kasaura, Naoto Onda, Yuta Oriike, Masaya Taniguchi, Akiyoshi Sannai, Sho Sonoda. #AI4Math #LeanProver #ITP
- The Leiden Declaration: Mathematics, AI, and making our values explicit. ~ Mateja Jamnik. #AI4Math
- Record type inference for dummies. ~ Gabriella Gonzalez. #Haskell #FunctionalProgramming
- Tagged data in Haskell (SICP 2.4.2). ~ kqr. #Haskell #FunctionalProgramming
- Learn you a Haskell for great good! (Miran Lipovaca's classic introduction to Haskell, ported to runnable Sabela notebooks). #Haskell #FunctionalProgramming