OpenAI Astra og AI-genererede beviser
OpenAI oplyser, at den interne Astra-model har skabt argumenterne bag ti nye matematiske resultater, som derefter er formaliseret i Lean. Resultaterne viser forskellen mellem AI-genereret opdagelse, maskinkontrollerede beviser og fagfællebedømmelse samt de praktiske kontrolbehov i forskning, uddannelse og organisationer.