IA inunda a matemática de provas e quebra seu sinal de profundidade
A matemática tratou por gerações a produção de teoremas como medida de sucesso: quanto mais profunda a prova, maior a conquista, e cargos e prêmios se baseiam nesses resultados. Em um texto de convidado no blog de Terence Tao, a matemática Bryna Kra argumenta que a IA rompeu esse sistema.
O teorema como sinal de profundidade
Para Kra, a produção de teoremas era um proxy de algo mais difícil de medir: o entendimento. Um grande avanço significava anos dedicados a aprender um assunto, revelar aspectos ocultos e tornar a resposta evidente à comunidade. Como teoremas profundos eram escassos e difíceis, funcionavam como mecanismo eficaz para identificar pensamento profundo - e, segundo ela, a IA quebrou esse sistema.
A IA reduziu o custo de produzir provas sofisticadas e, conforme os modelos melhoram, deve crescer a lista de conjecturas profundas que caem. Alguém com pouco conhecimento na área pode gerar um manuscrito que parece artigo polido, cita a literatura e combina técnicas que levariam anos para dominar. As máquinas produzem soluções mais rápido do que a comunidade consegue lê-las, muito menos digeri-las.
O caso da conjectura de Nivat
Kra relata que as mudanças chegaram à sua área nesta semana. A conjectura de Nivat, na interseção entre combinatória e sistemas dinâmicos, resistiu por quase três décadas. Ela a descreve com um grid infinito de ladrilhos de duas cores: se em toda janela retangular de n por m ladrilhos aparecem no máximo nm padrões, a coloração inteira se repete sob algum deslocamento fixo não nulo - periodicidade. Em trabalho divulgado em 2012, Van Cyr e ela provaram um resultado parcial: a periodicidade vale quando o número de padrões é no máximo metade da área da janela. Pouco depois, Jarkko Kari e Michal Szabados seguiram um caminho diferente, algébrico, com polinômios.
Havia um convite implícito a encontrar a ponte conceitual entre os métodos, mas as tentativas não deram certo. Sintetizar abordagens distintas é onde modelos de fronteira se destacam, observa Kra: a máquina não precisa de anos para absorver áreas diferentes antes de encontrar conexões, e pode traduzir notação, comparar resultados parciais e testar milhares de combinações. A conjectura foi proposta para inclusão no projeto Formal Conjectures, do Google DeepMind, tornando-se alvo de raciocínio automatizado.
Autoria, verificação e incentivos
Nesta semana, Kra recebeu vários supostos argumentos de prova da conjectura completa, de pesquisadores em sua primeira incursão no assunto. Alguns admitiram usar IA apenas para polir o inglês ou conferir a prova; nenhum aceitou explicar os argumentos por videochamada. O silêncio não significa que usaram IA, e prova proposta não é teorema. Divulgar o uso de IA e checar a correção, embora essenciais, perdem o ponto: mesmo corretos, os resultados abrem perguntas sobre o que se aprendeu, o que os autores contribuíram e qual será o impacto.
Uma prova, sustenta, é mais que um certificado de veracidade: é uma história, uma explicação, que destaca ideias novas e aponta direções. Ela cita Bill Thurston, que escreveu em 2010 no MathOverflow que o produto da matemática é clareza e entendimento, não os teoremas em si. Os novos textos contêm conhecimento, mas autoria humana envolve responsabilidade intelectual, compreensão e incorporação do resultado ao corpus da área.
Kra diz acolher provas geradas por IA e acreditar que provas exclusivamente humanas se tornarão raras. A questão, para ela, não é se máquinas devem participar da descoberta - já participam -, mas o que a comunidade passa a valorizar quando certos tipos de descoberta deixam de ser escassos. Revistas, comitês de contratação e de premiação não bastam: a revisão por pares é lenta, depende de um grupo pequeno e sobrecarregado, e o volume atual afoga os revisores.
Ela defende realinhar os incentivos: autores devem explicar o mecanismo da prova e como chegaram até ele; revistas precisam distinguir e creditar descoberta, prova, formalização e explicação; a exposição deve virar componente importante. Conceber o conceito certo e novas perguntas sempre fez parte do trabalho, mas é difícil de quantificar e foi tratado como subproduto. A matemática, escreve, é o canário na mina para toda a vida intelectual: como suas afirmações podem ser verificadas, assistimos à disrupção em tempo real, e áreas com evidência mais contestada terão de encontrar formas de avaliar o que é valioso em meio à produção abundante.