Chinese AI solves a 2014 math problem in 80 hours/IA china resuelve en 80 horas un problema matemático de 2014
Source
Recently, the DeepSeek team, based at Peking University, achieved a significant milestone in the field of artificial intelligence. Their model, DeepSeek-Prover-V1.5, successfully proved a mathematical theorem that had eluded the community for years. It was a problem in commutative algebra posed by the American mathematician Dan Anderson, which, obviously, I won't explain, mainly because I have no idea about commutative algebra.
Recientemente el equipo de DeepSeek, con sede en la Universidad de Pekín, ha conseguido un hito importante en el campo de la inteligencia artificial. Su modelo, DeepSeek-Prover-V1.5, logró demostrar un teorema matemático que había resistido los intentos de la comunidad durante años. Se trataba de un problema de álgebra conmutativa propuesto por el matemático estadounidense Dan Anderson que, obviamente, no os voy a decir en que consistía, principalmente por que no tengo ni idea de álgebra conmutativa.
To tackle such a complex problem, the DeepSeek team didn't limit themselves to a single approach. Instead, they designed a two-part system that combines the best of human strategy with the computing power of a machine. The system's "brain" is a 7-billion-parameter language model (DeepSeek-Prover-V1.5), specifically trained to reason in formal mathematical language. This model was fine-tuned using millions of synthetically generated problems and proofs, giving it an exceptional knowledge base in high school and university-level mathematics.
Para abordar un problema tan complejo, el equipo de DeepSeek no se limitó a un único enfoque. En lugar de eso, diseñó un sistema de dos partes que combina lo mejor de la estrategia humana y la potencia de cálculo de una máquina. El "cerebro" del sistema es un modelo de lenguaje de 7 mil millones de parámetros (DeepSeek-Prover-V1.5), entrenado específicamente para razonar en lenguaje matemático formal. Este modelo fue afinado usando millones de problemas y demostraciones creadas de forma sintética, lo que le da una base de conocimiento excepcional en matemáticas de nivel escolar y universitario.
Source
The real innovation is a strategic search engine called RMaxTS. This AI doesn't try to write a proof in one go. It uses an advanced technique called Monte Carlo Tree Search to intelligently explore multiple proof paths. The system works like a math whiz with an infinite notebook: the base model suggests the steps to take, while the RMaxTS engine evaluates millions of alternative paths in parallel, discarding those that don't work and delving deeper into the promising ones.
La verdadera innovación es un motor de búsqueda estratégica llamado RMaxTS. Esta IA no intenta escribir una demostración de una sola vez. Utiliza una técnica avanzada llamada búsqueda en árbol de Monte Carlo (Monte-Carlo Tree Search) para explorar múltiples caminos de demostración de forma inteligente. El sistema funciona como un genio de las matemáticas con una libreta infinita: el modelo base sugiere los pasos a seguir, mientras que el motor RMaxTS evalúa en paralelo millones de caminos alternativos, descartando los que no funcionan y profundizando en los prometedores.
In the case of the commutative algebra theorem, it is estimated that the system required 80 hours of computing time to traverse this enormous tree of possibilities and find the correct proof path. This achievement is much more than an anecdote; it is a clear indication of where artificial intelligence research is headed and how it could transform science. By automating verification and exploring complex proof paths, this technology lays the groundwork for a future where AI helps expand mathematical and scientific knowledge.
En el caso del teorema de álgebra conmutativa, se estima que el sistema necesitó 80 horas de computación para recorrer este enorme árbol de posibilidades y encontrar la ruta de demostración correcta. Este logro es mucho más que una anécdota; es una señal clara de hacia dónde se dirige la investigación en inteligencia artificial y cómo podría cambiar la ciencia. Al automatizar la verificación y explorar caminos de prueba complejos, esta tecnología sienta las bases para un futuro donde la IA ayude a expandir el conocimiento matemático y científico.
Source
The most obvious application of this milestone is the acceleration of mathematical research, allowing mathematicians to use these tools as intelligent assistants to explore conjectures, verify complex steps, or find proofs for problems that have remained unsolved for decades. It's like having a collaborator who knows all the literature and can test millions of hypotheses in parallel. Unlike an AI that generates text, one that proves theorems must construct an infallible logical chain of inference.
La aplicación mas obvia de este hito es la aceleración de la investigación matemática y que los matemáticos podrían usar estas herramientas como asistentes inteligentes para explorar conjeturas, verificar pasos complejos o encontrar demostraciones para problemas que llevan décadas sin resolverse. Es como tener un colaborador que conoce toda la literatura y puede probar millones de hipótesis en paralelo. A diferencia de una IA que genera texto, una que demuestra teoremas debe construir una cadena lógica de inferencia infalible.
Success with a difficult problem confirms that these models are beginning to develop a form of deep logical reasoning and long-term planning, a crucial skill for any general AI system. Unlike natural language responses, the proofs are written in a formal language, allowing a computer program to verify the proof's correctness 100%, eliminating any possibility of error or "hallucination" in the solution. The solution is not only found but also certified as correct.
El éxito con un problema difícil confirma que estos modelos están comenzando a desarrollar una forma de razonamiento lógico profundo y planificación a largo plazo, una habilidad crucial para cualquier sistema de IA general. A diferencia de las respuestas en lenguaje natural, las demostraciones se escriben en un lenguaje formal lo que permite que un programa informático verifique la corrección de la prueba al 100%, eliminando cualquier posibilidad de error o "alucinación" en la solución. La solución no solo se encuentra, sino que se certifica como correcta.
More information/Más información
https://www.plataformamedia.com/en/2026/04/13/china-ai-solves-math-problem-without-human-intervention-peking-university-2026/