Como propietario/mantenedor del sitio web de problemas de Erdős, un hilo con algunos comentarios sobre esta solución al #124: 1) Esta es una bonita prueba, que fue proporcionada por la AI a partir de la declaración formal sin intervención humana y luego formalizada en Lean. ¡Esto ya es impresionante!