OpenAI apresenta Astra com dez provas matemáticas verificadas em Lean, incluindo primeira construção de grupo não-sófico em 27 anos

OpenAI publicou em 1º de agosto um manuscrito de 249 páginas com certificados Lean 4 verificáveis por máquina pra dez novos resultados produzidos por uma versão interna de Astra — descrita como "our next major model" e não lançada — a custo estimado de ~US$ 2 mil em compute.