He empezado a publicar la serie Retos matemáticos en Lean 4.

La dinámica es sencilla: cada semana propondré un problema matemático para que quienes estén interesados compartan sus soluciones en Lean 4.

Al terminar la semana publicaré las soluciones del reto, que seguirán este esquema:

1. Una solución en lenguaje natural.
2. Varias formalizaciones en Lean 4, de menos a más detalladas:
   1. La más automática, generalmente con grind.
   2. Otras con tácticas más específicas, como norm_num, ring, positivity o linarith.
   3. Una demostración final en la que esas tácticas se sustituyen por lemas concretos.

Con este refinamiento sucesivo se pretende que la demostración final se corresponda, en la medida de lo posible, con la escrita en lenguaje natural.