Las matemáticas formales suelen estar fuera del alcance de muchos… pero eso está empezando a cambiar. Y no porque se simplifiquen, sino porque una IA ha aprendido a entenderlas y resolverlas paso a paso.
Se llama DeepSeek-Prover-V2 y viene de la startup china DeepSeek. Su misión: convertir enunciados informales —del tipo “demuestra que X implica Y”— en pruebas formales verificables utilizando Lean 4, el asistente matemático más exigente y preciso que hay.
🧠 De lo humano a lo lógico
El verdadero logro aquí no es que esta IA resuelva problemas. Es cómo lo hace: descomponiendo argumentos, razonando paso a paso y produciendo demostraciones validadas formalmente.
Un ejemplo típico: le das un problema del estilo AIME o Putnam, y en lugar de resolverlo con un número final, te devuelve un teorema formal estructurado como lo haría un matemático profesional. Pero en segundos.
📈 ¿Y qué tan buena es?
- 88,9% de éxito en el conjunto de pruebas MiniF2F-test.
- 49 problemas resueltos en el benchmark de nivel universitario PutnamBench.
- Incluso compite con su propio hermano mayor, DeepSeek-V3, en problemas del AIME 2025.
Nada mal para una IA que no está simplemente prediciendo palabras, sino razonando con lógica matemática.
🔓 Open-source y colaborativa
Y lo mejor: es de código abierto. Puedes encontrar DeepSeek-Prover-V2 en GitHub y en Hugging Face, listo para que desarrolladores, profes y matemáticos experimenten con él.
🧩 En Sombra Radio seguimos de cerca los modelos que no solo “responden”, sino que piensan con estructura. Porque el futuro no solo tiene que ver con parecer humano, también con razonar como uno.
