The readings shared in Bluesky on 7 November 2025 are:

• An introduction to formal real analysis (Lecture 16: Completeness of the real numbers). ~ Alex Kontorovich. #ITP #LeanProver #Math
• The path to a superhuman AI mathematician. ~ Lawrence Fisher. #AI #Math #ITP #LeanProver
• Math reasoning in times of AI: Lean way of theorem proving. ~ Jan Cepika et als. #ITP #LeanProver #Math #AI #LLM
• Babel-formal: Translation of proofs between Lean and Rocq. ~ Théo Stoskopf, Cyril Cohen, Nicolas Tabarea. #ITP #LeanProver #Rocq
• ScenicProver: A framework for compositional probabilistic verification of learning-enabled systems. ~ Eric Vin et als. #ITP #LeanProver
• Polynomial universes in Homotopy Type Theory. ~ C.B. Aberlé, David I. Spivak. #ITP #Agda #HoTT
• Mathematical exploration and discovery at scale. ~ Bogdan Georgiev, Javier Gómez-Serrano, Terence Tao, Adam Zsolt Wagner. #AI #Math #AlphaEvolve #ITP #LeanProver
• It’s the specification, stupid! (Seeking a significant shift in the traditional software development and verification paradigm). ~ Manfred Broy, Harald Ruess, Natarajan Shankar. #FormalVerification
• ¿Cuál es el siguiente término? ~ Miguel Ángel Morales. #Matemáticas
• #Exercitium: Mayores elementos de una matriz. #Haskell #ProgramaciónFuncional #Matemáticas