OpenAI diz que um modelo ainda não lançado resolveu dez problemas abertos de matemática e publicou as provas para as máquinas conferirem
Cada um dos dez resultados vem com um certificado formal em Lean 4 que compila sem lacunas; nenhum passou por revisão por pares, e o próprio Astra segue trancado dentro da empresa.
