OpenAI опубликовала 722 математических доказательства и рукописи

Компания OpenAI выпустила коллекцию из 722 математических рукописей, созданных нерелизной передовой языковой моделью. Значительная часть результатов содержит доказательства на языке Lean, а вычислительные затраты на каждый результат составили около трех часов работы в режиме ChatGPT Pro.