The readings shared in Bluesky on 14 August 2025 are

• Type inference for plain data. ~ Gabriella Gonzalez. #Haskell #FunctionalProgramming
• Type-machine (Using Template Haskell to derive the structure of records and simulate structural subtyping). ~ Arthur Jamet. #Haskell #FunctionalProgramming
• Using traversals to batch database queries. ~ Chris Penner. #Haskell #FunctionalProgramming
• The grind tactic. #ITP #LeanProver
• #Exercitium: Problemas de programación con Haskell (enero de 2016). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 13 August 2025 are

• In-order traversal in Haskell and Rust. ~ James Bowen. #Haskell #FunctionalProgramming #RustLang
• First analysis lecture (June 16, 2025). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Second analysis lecture "Filter" (June 17, 2025). ~ Alex Kontorovich. #ITP #LeanProver #Math
• Structures in Lean4 (June 20, 2025). ~ Filippo Nuccio. #ITP #LeanProver
• Blueprints and PNT (June 23, 2025). ~ Alex Kontorovich. #ITP #LeanProver
• The Infinity Project (How to use AI and mathematics to prove and improve science and security). ~ Patrick Shafto. #AI #Math #ITP #LeanProver
• Verificación formal en ACL2 de polinomios de múltiples variables y su aplicación al problema de la decisión en la lógica proposicional clásica. ~ Francisco Palomo Lozano. #ITP #ACL2 #Logic #Math
• Reseña de «The Infinity Project (How to use AI and mathematics to prove and improve science and security)». #AI #Math #ITP #LeanProver
• #Exercitium: Problemas de programación con Haskell (febrero de 2016). #Haskell #ProgramaciónFuncional #Matemáticas

En el artículo «The Infinity Project (How to use AI and mathematics to prove and improve science and security)» se propone invertir 112,5 MUSD en un concurso entre institutos de matemáticas para formalizar el conocimiento matemático en programas verificables. Con IA y lenguajes como Lean, se busca traducir y validar pruebas, democratizando el acceso a las matemáticas.

El objetivo es aplicar esta infraestructura para aumentar el rigor científico y reforzar la ciberseguridad. Formalizar teorías y procesos permitiría optimizar la investigación, prevenir fallos en sistemas críticos y reducir vulnerabilidades, con beneficios económicos y sociales significativos.

El plan incluye crear una amplia biblioteca matemática, entrenar IA para generar nuevo conocimiento útil y mostrar aplicaciones prácticas. Se plantea una colaboración entre academia, industria y gobiernos, con el potencial de abrir nuevas industrias y transformar ciencia, tecnología y seguridad.

The readings shared in Bluesky on 9 August 2025 are

• Mission-time Linear Temporal Logic Formula Progression (in Isabelle/HOL). ~ Katherine Kosaian, Zili Wang. #ITP #IsabelleHOL
• Two-way deterministic finite automata (in Isabelle/HOL). ~ Felipe Escallón, Tobias Nipkow. #ITP #IsabelleHOL
• Truly functional solutions to the longest uptrend problem (Functional pearl). ~ Alexander Dinges, Ralf Hinze. #Haskell #FunctionalProgramming
• Teaching introductory functional programming using Haskelite. ~ Pedro Vasconcelos. #Haskell #FunctionalProgramming
• Macros in Prolog: Term and goal expansion. ~ Markus Triska. #Prolog #LogicProgramming
• Mathematicians question AI performance at International Math Olympiad. ~ Emily Riehl. #AI #Math #IMO
• Geoint-R1: Formalizing multimodal geometric reasoning with dynamic auxiliary constructions. ~ Jingxuan Wei et als. #ITP #LeanProver #LLMs
• #Exercitium: Problemas de programación con Haskell (diciembre de 2016). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 10 August 2025 are

• A practical formalization of monadic equational reasoning in dependent-type theory. ~ Reynald Affeldt, Jacques Garrigue, Takafumi Saikawa, #ITP #CoqProver
• Domain-specific tensor languages. ~ Jean-Philippe Bernardy, Patrik Jansson. #Haskell #FunctionalProgramming
• Binary search—think positive. ~ Alexander Dinges, Ralf Hinze. #ITP #Agda #FunctionalProgramming
• GradSTL: Comprehensive signal temporal logic for neurosymbolic reasoning and learning. ~ Mark Chevallier, Filip Smola, Richard Schmoetten, Jacques D. Fleuriot. #ITP #IsabelleHOL
• A contextual formalization of structural coinduction. ~ Paul Downen, Zena M. Ariol. #FunctionalProgramming
• OCaml Blockly. ~ Kenichi Asai. #OCaml #FunctionalProgramming
• The graphical theory of monads. ~ Ralf Hinze, Dan Marsden. #CategoryTheory
• #Exercitium: Problemas de programación con Haskell (noviembre de 2016). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (mayo de 2016). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 8 August 2025 are

• Discrete mathematics with Lean 4. ~ Shrey Vivek./#/g/shreyvivek/gamemaker #ITP #LeanProver #Math
• Gödel's incompleteness theorem. ~ Thorsten Altenkirch. #ITP #LeanProver #Logic #Math
• Scrutinizing LLM reasoning models (Researchers are seeking to learn the steps behind an LLM's inference process). ~ Emma Stamm. #LLMs #Reasoning
• Cálculo infinitesimal. ~ Gerard Romo Garrido. #eBook #Matemáticas
• #Exercitium: Problemas de programación con Haskell (febrero de 2017). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (enero de 2017). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 7 August 2025 are

• Thinking machines: Mathematical reasoning in the age of LLMs. ~ Andrea Asperti, Alberto Naibo, Claudio Sacerdoti Coen. #AI #LLMs #Math #ITP #LeanProver
• Goedel-Prover-V2: Scaling formal theorem proving with scaffolded data synthesis and self-correction. ~ Yong Lin et als. #LLMs #AI #ITP #LeanProver #Math

The readings shared in Bluesky on 6 August 2025 are

• A comparative study of neurosymbolic AI approaches to interpretable logical reasoning. ~ Michael K. Chen. #Neurosymbolic #AI
• #Exercitium: Problemas de programación con Haskell (noviembre de 2017). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (junio de 2017). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (mayo de 2017). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (abril de 2017). #Haskell #ProgramaciónFuncional #Matemáticas
• #Exercitium: Problemas de programación con Haskell (marzo de 2017). #Haskell #ProgramaciónFuncional #Matemáticas

The readings shared in Bluesky on 5 August 2025 are

• Simons Foundation Lean Workshop. ~ Antoine Chambert-Loir Alex Kontorovich, Heather MacBeth. #ITP #LeanProver #Math
• First analysis lecture (June 16, 2025) ~ Alex Kontorovich. #ITP #LeanProver #Math
• Doing elementary number theory in Lean. ~ Antoine Chambert-Loir #ITP #LeanProver #Math
• Doing elementary number theory in Lean (Video 1). ~ Antoine Chambert-Loir #ITP #LeanProver #Math
• Doing elementary number theory in Lean (Video 2). ~ Antoine Chambert-Loir #ITP #LeanProver #Math
• First geometry lecture (June 17, 2025). ~ Heather Macbeth. #ITP #LeanProver #Math
• Second geometry lecture (June 18, 2025). ~ Heather Macbeth. #ITP #LeanProver #Math
• Second analysis lecture "Filter" (June 17, 2025) ~ Alex Kontorovich. #ITP #LeanProver #Math
• A crash course on type theory. ~ Antoine Chambert-Loir. #ITP #LeanProver #TypeTheory
• A crash course on type theory (Video). ~ Antoine Chambert-Loir. #ITP #LeanProver #TypeTheory
• Structures in Lean4 (June 20, 2025). ~ Filippo Nuccio. #ITP #LeanProver
• Blueprints and PNT (June 23, 2025). ~ Alex Kontorovich. #ITP #LeanProver
• Simple groups in Lean. ~ Antoine Chambert-Loir. #ITP #LeanProver #Math
• Simple groups in Lean (Video). ~ Antoine Chambert-Loir. #ITP #LeanProver #Math
• Metaprogramming in Lean, Talk 1 (June 23, 2025). ~ Heather Macbeth. #ITP #LeanProver
• Metaprogramming in Lean, Talk 2 (June 24, 2025). ~ Heather Macbeth. #ITP #LeanProver
• Metaprogramming in Lean, Talk 3 (June 25, 2025). ~ Heather Macbeth. #ITP #LeanProver
• The Lean FRO year 3 roadmap. #ITP #LeanProver

The readings shared in Bluesky on 4 August 2025 are

• Cobblestone: Iterative automation for formal verification. ~ Saketh Ram Kasibatla, Arpan Agarwal, Yuriy Brun, Sorin Lerner, Talia Ringer, Emily First. #ITP #CoqProver #AI #LLMs
• Reflections on Haskell@Meta. ~ Simon Marlow. #Haskell #FunctionalProgramming