La IA generativa alucina, lo que genera un problema de veracidad que la ciencia no puede permitirse. El científico computacional Tudor Achim cree que una idea de hace 400 años contiene la solución: el sueño de Leibniz de un marco lógico donde los errores son simplemente imposibles. Conozca su propuesta de superinteligencia matemática que anclaría la IA en la verificación formal, transformando a los chatbots poco fiables en socios rigurosos para el descubrimiento científico.

El camino hacia la superinteligencia matemática

Mathematics has driven progress for thousands of years, but today, human verification can't keep up with the accelerating pace of AI-generated proofs. Legendary problems like the Poincaré conjecture took years for global teams to validate, while modern AI can now solve Olympiad-level challenges in hours. A 400-year-old vision of formalized logic, now realized through tools like Lean and Mathlib, promises certainty and trust in mathematical results. This shift lets humanity focus on creativity and exploration, while AI handles precision and proof verification.

AI And Formal Math Will End The Human Bottleneck In Discovery

For 4,000 years, math has relied on human trust and peer review, but the explosion of AI-generated proofs now overwhelms expert capacity to verify them. Legendary problems like the Poincaré conjecture already required years of collective scrutiny. A new era is emerging, where computers use formal languages like Lean to check proofs with absolute certainty. This shift could enable AI to collaborate reliably with humans, replacing tedious checking with creative exploration.