Публикацията от 6 октомври
OpenAI обяви нови математически резултати от свой вътрешен модел и публикува материали в GitHub. Компанията предоставя и формализации на много доказателства в Lean, както и информация за изследователския процес. Това позволява обсъждането да се насочи към конкретни артефакти, вместо единствено към демонстрация на възможности.
Какво показва хранилището
README на openai/math изрично предупреждава, че материалите са на различни етапи на проверка. Не всички имат Lean формализация, а неформализирани резултати могат да съдържат проблеми. При проверката ни колекцията посочва 719 ръкописа в 372 тематични семейства и приблизително 42% формализирани основни резултати. Тези числа описват текущия каталог и могат да се променят.
Нашият редакционен прочит
Достъпният ръкопис и проверимият формален артефакт са различни степени на доказателствена опора. Затова не представяме цялата колекция като окончателно потвърдена. За оценката на отделен резултат са важни постановката, допусканията и конкретната проверка. Това съобщение само по себе си не означава, че същият вътрешен модел е достъпен в обичайния ChatGPT акаунт.
