IA resolve em dias problema que matemáticos tentaram resolver por anos

Gauss, sistema de IA da Math, Inc., resolveu em cinco dias o problema do empacotamento de esferas em oito dimensões, seguindo o roteiro da equipe.
A equipe liderada por Sidharth Hariharan e a matemática Maryna Viazovska tentaram formalizar a prova passo a passo, mas receberam a notícia de que alguém já havia chegado lá.
A notícia se insere em uma corrida entre empresas de IA para resolver problemas matemáticos abertos, com avanços recentes da OpenAI e do Google DeepMind.
Matemáticos destacam benefícios da IA, porém pedem cautela sobre transparência, crédito aos autores humanos e limites da tecnologia.
O grupo segue trabalhando para tornar o código utilizável e planeja futuras aplicações, com Hariharan pretendendo formalizar o próximo teorema por conta própria.

O Gauss, um sistema de IA desenvolvido pela startup Math, Inc., resolveu em dias o problema do empacotamento de esferas em oito dimensões, tarefa que levou matemáticos anos para avançar. A conclusão ocorreu após a equipe de Hariharan formalizar a demonstração de Viazovska, usando o software Lean.

Sidharth Hariharan, estudante de pós-graduação em matemática na Universidade Carnegie Mellon, recebeu a notícia e compartilhou o momento com o orientador. A campanha de formalização envolveu seis matemáticos ao longo de mais de dois anos, que buscaram detalhar a prova de Viazovska passo a passo.

Pouco antes, Viazovska já tinha informado que alguém havia chegado lá primeiro. A equipe de Hariharan dedicou-se a estruturar a demonstração, enquanto a IA, alimentada pelo roteiro elaborado, concluiu a tarefa em cinco dias.

A investigação envolve o esforço de várias empresas de tecnologia que buscam sistemas de raciocínio capazes de lidar com problemas matemáticos complexos. A trajetória inclui avanços recentes de grandes players como OpenAI e Google DeepMind, que anunciaram resultados em teoremas abertos e soluções para problemas diversos.

No encontro entre humanos e IA, os autores destacam que a colaboração pode acelerar descobertas. No entanto, surgem questionamentos sobre crédito, transparência de métodos e a relação entre automação e trabalho humano na matemática.

A trajetória da equipe começou com o desejo de formalizar a prova de Viazovska, que demonstrou o empacotamento de esferas em oito dimensões. Inicialmente, o grupo usou Lean para estruturar a lógica, enquanto a Math, Inc. investigava melhorias do Gauss para avançar o projeto.

Em outubro passado, a empresa apresentou o Gauss como a versão que poderia avançar significativamente. O resultado, confirmado meses depois, mostrou que o sistema foi capaz de concluir toda a demonstração da prova de Viazovska, conforme relatos internos.

Após a confirmação, o grupo avaliou o impacto do feito. Houve reações mistas entre acadêmicos, com avanços reconhecidos, mas a necessidade de mais tempo para tornar o código utilizável de forma ampla e confiável. Hariharan sinalizou que o objetivo original do projeto permanece em aberto.

Entre os envolvidos, há debates sobre a dependência de IA para resolver problemas centrais da matemática. A comunidade destaca que o trabalho humano continua essencial para validar, interpretar e aperfeiçoar o que a IA produz.

Poiroux, doutorando na École Polytechnique, explicou que a equipe retomou o estudo com foco em aprimorar a formalização, removendo redundâncias e tornando a demonstração mais acessível. Hariharan afirmou que o aprendizado obtido supera meras automatizações.

O episódio também reacende a discussão sobre o financiamento e o equilíbrio de poder entre laboratórios acadêmicos e startups de IA. Especialistas ressaltam o valor humano na matemática e a importância de crédito adequado a pesquisadores.

Para Hariharan, o próximo desafio é formalizar um novo teorema por conta própria, após a experiência com o Gauss. Ele acompanha projetos na Axiom Math neste verão, mas já planeja retomar estudos com foco em futuras demonstrações autossuficientes.