Formalizan en Lean la solución del problema de Hopf: la esfera de seis dimensiones admite una estructura compleja
Formalization of the Solution to the Hopf Problem
El repositorio HopfProblem de GitHub presenta una formalización en Lean de la resolución del problema de Hopf, demostrando que la esfera de seis dimensiones admite una estructura de variedad compleja compatible con su topología estándar. El proyecto se basa en el artículo de Levent Alpöge y utiliza el asistente de pruebas Lean, con soporte para verificación en línea.
La esfera de seis dimensiones admite una estructura de variedad compleja compatible con su topología estándar.