He empezado a publicar la serie de "Retos matemáticos en Lean 4" en el canal de Retos matemáticos de Telegram.

La dinámica es sencilla: cada semana publicaré un problema matemático para que los interesados compartan sus soluciones en Lean 4 dentro del grupo. Aunque el acceso es público y cualquiera puede leer los retos, es necesario unirse al grupo en https://t.me/Retos_Matematicos para publicar soluciones.

Al finalizar de la semana publicaré un enlace a Lean Web con las soluciones del reto, que seguirán el siguiente esquema: en primer lugar, una solución en lenguaje natural; a continuación, varias formalizaciones en Lean 4 empezando por la más automática (generalmente, con grind), siguiendo con otras con tácticas más específicas (como norm_num, ring, positivity, linarith) y terminando con una demostración en que la que dichas tácticas se sustituyen por lemas concretos. Con este proceso de refinamiento sucesivo se buscará que la demostración final se corresponda, en la medida de lo posible con la escrita en lenguaje natural.

Una vez concluido cada reto, publicaré las soluciones en este blog bajo la etiqueta Retos Lean4.