Dois subagentes desenvolveram as ideias matemáticas centrais do trabalho. Outros 13 contribuíram com sugestões, 30 não conseguiram criar novas ideias, 13 verificaram os argumentos e dois ajudaram a redigir o artigo inicial.
Dois matemáticos da Anthropic confirmaram o resultado, que foi formalizado com o Lean. O Lean é um programa de código aberto usado para verificar demonstrações matemáticas.
IA já aparece em outros resultados matemáticos
Modelos de linguagem também foram usados neste ano para resolver problemas de Erdős, uma série de questões matemáticas. A OpenAI divulgou recentemente dez resultados obtidos por seu modelo interno Astra.
Outro trabalho ligado à Anthropic refutou a conjectura jacobiana, um problema antigo da matemática. Os avanços reacenderam o debate sobre autoria e responsabilidade em pesquisas feitas com inteligência artificial.
Matemáticos assinaram em junho uma declaração que defende provas atribuídas a autores responsáveis por sua correção. O vencedor da Medalha Fields Timothy Gowers escreveu: “Se chegarmos a um mundo em que teoremas matemáticos não sejam mais associados a matemáticos, talvez isso não seja mais problemático do que o fato de estrelas não receberem nomes de astrônomos.”