Новость · ИИ и программы
OpenAI опубликовала математические рукописи и доказательства в Lean
Опубликовано на USB.RU:
В публичном репозитории openai/math собраны результаты внутренней модели и артефакты проверки. В октябрьском снимке каталога: 719 рукописей в 372 семействах.
Каталог обновляется: в первых сообщениях было 722 рукописи. Не у каждой работы есть формализация в Lean; README предупреждает об ошибках в неформализованных результатах. Lean проверяет доказательство по записанным правилам, а новизну математического результата оценивают исследователи.