O Gauss, um sistema de IA desenvolvido pela startup Math, Inc., resolveu em dias o problema do empacotamento de esferas em oito dimens\u00f5es, tarefa que levou matem\u00e1ticos anos para avan\u00e7ar. A conclus\u00e3o ocorreu ap\u00f3s a equipe de Hariharan formalizar a demonstra\u00e7\u00e3o de Viazovska, usando o software Lean.<\/p>\n
Sidharth Hariharan, estudante de p\u00f3s-gradua\u00e7\u00e3o em matem\u00e1tica na Universidade Carnegie Mellon, recebeu a not\u00edcia e compartilhou o momento com o orientador. A campanha de formaliza\u00e7\u00e3o envolveu seis matem\u00e1ticos ao longo de mais de dois anos, que buscaram detalhar a prova de Viazovska passo a passo.<\/p>\n
Pouco antes, Viazovska j\u00e1 tinha informado que algu\u00e9m havia chegado l\u00e1 primeiro. A equipe de Hariharan dedicou-se a estruturar a demonstra\u00e7\u00e3o, enquanto a IA, alimentada pelo roteiro elaborado, concluiu a tarefa em cinco dias.<\/p>\n
A investiga\u00e7\u00e3o envolve o esfor\u00e7o de v\u00e1rias empresas de tecnologia que buscam sistemas de racioc\u00ednio capazes de lidar com problemas matem\u00e1ticos complexos. A trajet\u00f3ria inclui avan\u00e7os recentes de grandes players como OpenAI e Google DeepMind, que anunciaram resultados em teoremas abertos e solu\u00e7\u00f5es para problemas diversos.<\/p>\n
No encontro entre humanos e IA, os autores destacam que a colabora\u00e7\u00e3o pode acelerar descobertas. No entanto, surgem questionamentos sobre cr\u00e9dito, transpar\u00eancia de m\u00e9todos e a rela\u00e7\u00e3o entre automa\u00e7\u00e3o e trabalho humano na matem\u00e1tica.<\/p>\n
A trajet\u00f3ria da equipe come\u00e7ou com o desejo de formalizar a prova de Viazovska, que demonstrou o empacotamento de esferas em oito dimens\u00f5es. Inicialmente, o grupo usou Lean para estruturar a l\u00f3gica, enquanto a Math, Inc. investigava melhorias do Gauss para avan\u00e7ar o projeto.<\/p>\n
Em outubro passado, a empresa apresentou o Gauss como a vers\u00e3o que poderia avan\u00e7ar significativamente. O resultado, confirmado meses depois, mostrou que o sistema foi capaz de concluir toda a demonstra\u00e7\u00e3o da prova de Viazovska, conforme relatos internos.<\/p>\n
Ap\u00f3s a confirma\u00e7\u00e3o, o grupo avaliou o impacto do feito. Houve rea\u00e7\u00f5es mistas entre acad\u00eamicos, com avan\u00e7os reconhecidos, mas a necessidade de mais tempo para tornar o c\u00f3digo utiliz\u00e1vel de forma ampla e confi\u00e1vel. Hariharan sinalizou que o objetivo original do projeto permanece em aberto.<\/p>\n
Entre os envolvidos, h\u00e1 debates sobre a depend\u00eancia de IA para resolver problemas centrais da matem\u00e1tica. A comunidade destaca que o trabalho humano continua essencial para validar, interpretar e aperfei\u00e7oar o que a IA produz.<\/p>\n
Poiroux, doutorando na \u00c9cole Polytechnique, explicou que a equipe retomou o estudo com foco em aprimorar a formaliza\u00e7\u00e3o, removendo redund\u00e2ncias e tornando a demonstra\u00e7\u00e3o mais acess\u00edvel. Hariharan afirmou que o aprendizado obtido supera meras automatiza\u00e7\u00f5es.<\/p>\n
O epis\u00f3dio tamb\u00e9m reacende a discuss\u00e3o sobre o financiamento e o equil\u00edbrio de poder entre laborat\u00f3rios acad\u00eamicos e startups de IA. Especialistas ressaltam o valor humano na matem\u00e1tica e a import\u00e2ncia de cr\u00e9dito adequado a pesquisadores.<\/p>\n
Para Hariharan, o pr\u00f3ximo desafio \u00e9 formalizar um novo teorema por conta pr\u00f3pria, ap\u00f3s a experi\u00eancia com o Gauss. Ele acompanha projetos na Axiom Math neste ver\u00e3o, mas j\u00e1 planeja retomar estudos com foco em futuras demonstra\u00e7\u00f5es autossuficientes.<\/p>\n","protected":false},"excerpt":{"rendered":"