An introduction to formal real analysis (Lecture 16: Completeness of the real numbers). ~ Alex Kontorovich. youtu.be/omfZbs2v_dQ #ITP #LeanProver #Math

The path to a superhuman AI mathematician. (Mathematics is the first place where evidence of AI superintelligence is likely to appear, a theoretical computer scientist says). ~ Lawrence Fisher. cacm.acm.org/news/the-pat... #AI #Math #ITP #LeanProver

Polynomial universes in Homotopy Type Theory. ~ C.B. Aberlé, David I. Spivak. arxiv.org/abs/2409.19176 #ITP #Agda #HoTT

Babel-formal: Translation of proofs between Lean and Rocq. ~ Théo Stoskopf, Cyril Cohen, Nicolas Tabarea. hal.science/hal-05342510... #ITP #LeanProver #Rocq

ScenicProver: A framework for compositional probabilistic verification of learning-enabled systems. ~ Eric Vin et als. arxiv.org/abs/2511.021... #ITP #LeanProver

Math reasoning in times of AI: Lean way of theorem proving. ~ Jan Cepika et als. home.zcu.cz/~danek/DATA/... #ITP #LeanProver #Math #AI #LLM

It’s the specification, stupid! (Seeking a significant shift in the traditional software development and verification paradigm). ~ Manfred Broy, Harald Ruess, Natarajan Shankar. dl.acm.org/doi/full/10.... #FormalVerification

Mathematical exploration and discovery at scale. ~ Bogdan Georgiev, Javier Gómez-Serrano, Terence Tao, Adam Zsolt Wagner. arxiv.org/abs/2511.028... #AI #Math #AlphaEvolve #ITP #LeanProver

¿Cuál es el siguiente término? ~ Miguel Ángel Morales. www.gaussianos.com/cual-es-el-s... #Matemáticas

"Así como no sentimos la salud de todo nuestro cuerpo sino solo el punto donde nos aprieta el zapato, tampoco pensamos en todos nuestros asuntos que marchan perfectamente bien sino en alguna pequeñez insignificante que nos disgusta." ~ Arthur Schopenhauer (1788-1860).

"Quiero que cada mañana sea para mi año nuevo. Cada día quiero echar cuentas conmigo mismo, y renovarme cada día." ~ Antonio Gramsci (1891-1937).

Readings shared November 5, 2025. jaalonso.github.io/vestigium/po... #AI #FunctionalProgramming #Haskell #ITP #LeanProver #Math

#Exercitium: Último dígito no nulo del factorial. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas

#Exercitium: Repetición de elementos. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional

#Exercitium: Conjunto de primos relativos. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas

Formalizing Schwartz functions and tempered distributions. ~ Moritz Doll. arxiv.org/abs/2510.240... #ITP #LeanProver #Math

Tree-based premise selection for Lean4. ~ Zichen Wang, Anjie Dong, Zaiwen Wen. openreview.net/pdf?id=omyNP... #ITP #LeanProver #AI

"Mathlib has reached 2 million lines of code as of October 28. Thanks to everyone that contributed to Mathlib during the roughly 8 years of Mathlib's existence!" https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/2.20million/near/553410451 #leanprover #mathlib

"Tal vez haya algo peor que los sueños desvanecidos: perder la voluntad de volver a soñar." ~ Sigmund Freud (1856-1939).

Readings shared November 4, 2025. jaalonso.github.io/vestigium/po... #AI #ITP #LeanProver #Math

Quel sera l’impact de l’IA sur les mathématiques dans les prochaines années? - Timothy Gowers youtu.be/bcTWVUueai4 #AI #Math #ITP #LeanProver

Is this the end of handwritten math? Introducing Lean. ~~~ Ank Yog. youtu.be/0QZI_m8WZ0Q #ITP #LeanProver #Math

"Lo que sentimos depende en un grado enorme e insospechado de lo que pensamos." ~ Alan Watts (1915-1973).

Readings shared November 2, 2025. jaalonso.github.io/vestigium/po... #AI #Agda #Automath #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LCF #LLM #LeanProver #Physics #TypeTheory

"Why don't you use dependent types?" ~ Lawrence Paulson. lawrencecpaulson.github.io//2025/11/02/... #ITP #Automath #LCF #IsabelleHOL #LeanProver #TypeTheory

Property-based testing for asynchronous functional reactive programming using linear temporal logic. ~ Christian Emil Nielsen, Mathias Faber Kristiansen, Patrick Bahr. bahr.io/pubs/files/p... #Haskell #FunctionalProgramming

Lean4Physics: Comprehensive reasoning framework for college-level Physics in Lean4. ~ Yuxin Li et als. arxiv.org/abs/2510.260... #ITP #LeanProver #Physics #AI #LLM

On graded coeffect types for information-flow control. ~ Vilem-Benjamin Liepelt et als. granule-project.github.io/papers/secur... #ITP #Agda

"He dejado de acordarme de lo que ayer ocurrió y de preguntarme qué ocurrirá mañana. Lo que ocurre hoy, en el minuto presente, es lo que me interesa." ~ Nikos Kazantzakis (1883-1957).

Readings shared November 1, 2025. jaalonso.github.io/vestigium/po... #Agda #FunctionalProgramming #Haskell #ITP #LeanProver #Math

#Exercitium: Precio total. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional

An introduction to formal real analysis (Lecture 15: The real numbers). ~ Alex Kontorovich. youtu.be/U-xG56YHCiE #ITP #LeanProver #Math

Call-by-value and call-by-name: A simple proof of a classic theorem. ~ D. Biernacki, J. McKinna, & F. Sieczkowski. pure.hw.ac.uk/ws/portalfil... #ITP #Adga #FunctionalProgramming

Formalization of coverage checking in Agda. ~ Satoshi Takimoto, Sosuke Moriguchi, Takuo Watanabe. wasabi315.github.io/files/wctp20... #ITP #Agda #FunctionalProgramming

"Todos los placeres son quiméricos. Conviene una total moderación porque precisamente el afán y lucha por la felicidad, el lujo y el placer es lo que provoca las grandes desgracias. Ser feliz no es difícil sino totalmente imposible." ~ Arthur Schopenhauer (1788-1860).

Readings shared October 31, 2025. jaalonso.github.io/vestigium/po... #AI #Autoformalization #CompSci #Education #FunctionalProgramming #GenAI #Haskell #ITP #LeanProver #Math #Physics

#Exercitium: Extensión de un fichero. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional

GenAI for computing careers: A sunny take (Positive outcomes for computer science graduates will take some determined action from both educators and learners). ~ Saurabh Bagchi. cacm.acm.org/blogcacm/gen... #GenAI #CompSci #Education

Conjecture extraction for proof autoformalization. ~ Simon Sorg, Wenda Li, Soumya Banerjee. www.researchgate.net/profile/Soum... #AI #Math #ITP #LeanProver #Autoformalization

Virasoro algebra and Sugawara constructions formally in Lean. ~ Kalle Kytölä. arxiv.org/abs/2510.21741 #ITP #LeanProver #Math

Derivation of fundamental physical constants from substrate ontology. ~ Matthew Scherf. philpapers.org/archive/SCHD... #ITP #LeanProver #Physics

Accelerating discovery with the AI for Math Initiative (The initiative brings together some of the world's most prestigious research institutions to pioneer the use of AI in mathematical research). ~ Pushmeet Kohli, Eugénie Rives. blog.google/technology/g... #AI #Math

"Quien no es feliz con poco no lo será con mucho." ~ Lao-Tse (siglo VI a.n.e.).

Readings shared October 30, 2025. jaalonso.github.io/vestigium/po... #FunctionalProgramming #Haskell #ITP #LeanProver #Math

#Exercitium: Distancia de Hamming. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas

#Exercitium: Rompecabeza matemático. jaalonso.github.io/exercitium/p... #Haskell #ProgramaciónFuncional #Matemáticas

Lists are geometric series. ~ iacgm. iacgm.com/articles/adts/ #Haskell #FunctionalProgramming

Formalization of Auslander--Buchsbaum--Serre criterion in Lean4. ~ Naillin Guan, Yongle Hu. arxiv.org/abs/2510.24818 #ITP #LeanProver #Math

#MULCIA: Postdoc and PhD positions in symbolic AI at TU Wien. tinyurl.com/26ulorxb #PhD #PostDoc #CompSci #AI

Readings shared October 29, 2025. jaalonso.github.io/vestigium/po... #AI #CompSci #FunctionalProgramming #GenAI #HOL_Light #Haskell #ITP #IsabelleHOL #LeanProver #Logic #Math #Metamath #Mizar #Programming #Python #Rocq