BREAKING: Споживча версія Арістотеля розбиває Патнама, розв'язуючи та офіційно перевіряючи 10/12 задач у @leanprover. Вітаємо аматорів-математиків @namrata_anand2, які використали споживчу версію Арістотеля з раннім публічним випуском задач. Схоже, що Арістотель їв їх на сніданок, розв'язавши 10/12 повністю автономно. Зараз ми вивчаємо ці файли і поділимося детальніше пізніше, але зараз варто звернути увагу на дві корисні речі: ▪️Це, схоже, перші повністю формалізовані рішення проблем Патнама 2025 року, оприлюднені публічно. ▪️Усі вони використовували нещодавно випущений інтерфейс природної мови, у якому Арістотель передавав питання природною мовою, потім автоматично формалізував його у твердження Lean4, а потім повністю автономно завершував доказ без людини в циклі. Раніше ми зосереджувалися на сучасних здібностях доведення теорем Арістотеля, але вони також набувають значних здібностей до автоформалізації. Ми вступаємо в новий світанок для штучного інтелекту та математики. Повільно... А потім все одразу!