Lean y Agda

Este fin de semana me puse a jugar un poco en Lean y Agda. Quería empezar a jugar el HoTT game. Pero además tenía ganas de meterme en problemas, así que me puse a hacer el build de emacs 27 para ponerle el doom emacs que recomendaron los autores del juego. Es la primera vez que hago un build en mi vida. Aunque todo fue automático gracias al make, configure y autogen, igual fue una aventura. También instalé Lean, aunque con el VScode. A ver si logro echar a andar Lean en emacs para poder desinstalar esta wea microsoftiana. Se siente raro.

Por ahora me trato de acostumbrar a la mathlib de Lean 3, esperando poder hacer algo interesante un día no tan lejano. Quizá formalizar las pruebas en marcos que tanto le gustan a Ángel.

También quisiera retomar el tutorial de Coq de software foundations. Debe seguir por ahí en mi computadora. Aunque acabo de encontrar otro tutorial de Coq.

Los primeros dos niveles del HoTT game en Agda fueron divertidos. Eso del transporte a lo largo de trayectorias está muy loco. En el juego, definí el espacio de bucles ΩS¹ de S¹ y construí funciones entre Z y ΩS¹. Luego seguirá probar que son inversas y, por lo tanto, una equivalencia. Estoy muy emocionado. ¿Las cosas de la escuela? Bien, gracias, siguiente pregunta.

No encuentro tablas de valores críticos para las pruebas de bondad de ajuste de Kolmogorov-Smirnov y de Kuiper. Muchas fuentes incluso parece que las confunden o usan definiciones que creo que son conflictivas. Moriré.

Me pasaré a lo que sigue.

También está lo de ecuaciones diferenciales. Eso se ve más divertido, pero no he avanzado mucho. Oh, y las tareas de análisis. Y las de inferencia. Moriré.

Ah, y descubrí un hack de python 2. Adjunto imagen.