No puedo creer que los humanos escriban código Lean manualmente, hombre. Y que las cosas se estaban formalizando en él antes de los LLMs. Formalizar cualquier cosa en Lean se siente tan placentero como pelarse la piel con un pelador de patatas y tan interesante como ver secar la pintura.

No me hables de "la alegría del juego" / "es tan interactivo" o lo que sea. Hay juegos con cosas por todas partes, así como hay ra*e por todas partes, y sé la diferencia.

@notmoeezm "No me importa ni un carajo si las máquinas verifican pruebas" fuente: tipo que ajusta algoritmos de búsqueda en el espacio de pruebas por diversión, usando Lean😞