A OpenAI anunciou que uma versão interna do modelo Astra resolveu 10 problemas em aberto nas áreas de matemática e computação teórica. A operação exigiu cerca de 2.000 dólares em poder computacional, tendo os resultados sido publicados no GitHub sob a forma de provas formais verificáveis na linguagem Lean.
O elemento central deste avanço não é apenas a resolução dos problemas em si, mas a mudança do método de entrega. Ao recorrer à linguagem Lean, o modelo abandona o terreno estritamente probabilístico do texto em linguagem natural para gerar provas matematicamente determinísticas que qualquer computador pode auditar de forma autónoma.
Com um custo computacional reduzido para solucionar questões complexas, a dinâmica do I&D científico e tecnológico altera-se. A validação deixa de estar dependente do tempo de revisão manual para se tornar instantânea, o que desloca o estrangulamento do processo da verificação para a capacidade de formalizar as perguntas certas.
A transição de modelos de síntese para sistemas que produzem matemática auditável reduz o custo da descoberta em setores intensivos em cálculo. O fator determinante deixa de ser a quantidade de horas dedicadas à verificação e passa a ser a habilidade em traduzir problemas do mundo real para ambientes formais de prova.