A IA generativa alucina, criando um problema de confiabilidade que a ciência não pode se dar ao luxo de ignorar. O cientista da computação Tudor Achim acredita que uma ideia de 400 anos oferece a solução: o sonho de Leibniz de um sistema lógico em que erros sejam simplesmente impossíveis. Conheça sua proposta de uma superinteligência matemática capaz de fundamentar a IA na verificação formal, transformando chatbots pouco confiáveis em parceiros rigorosos para a descoberta científica.

O caminho para a superinteligência 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.