🚀 Алеф-провер щойно перейшов у РЕЖИМ ЗВІРА 4 математичні задачі, які не були розв'язані протягом 20+ років. Формальні докази в Lean 4. Менше 48 годин. Менше 5 тисяч доларів загалом. ✅ Гіпотеза про біноміальні межі хвоста (Telgarsky, 2009) ✅ Наближення ґратки квантових затворів (Грін і Дамелін, 2015)* ✅ Ердьош 124 ✅ Ердьош 481 ✅ #1 у таблиці лідерів PutnamBench Епоха AI-математики настав. Особлива подяка @BorisHanin та @ylecun за допомогу втілити це 🙏 в життя І величезна подяка команді @LeanFRO — нічого з цього неможливо без неймовірної основи, яку ви створили. Aleph незабаром стане доступним для публіки, слідкуйте за оновленнями! *за умови результатів Сардарі (2015), формалізація очікує

Наш агент з перевірки Aleph щойно досяг #1 на PutnamBench — бенчмарку, побудованому на основі задач Putnam — однієї з найскладніших олімпіади з математики на рівні коледжу — повністю формалізованої з машинно перевіреними доказами без участі людини. Задачі Патнама часто вважаються складнішими, ніж задачі Мої Мо, і охоплюють широкий спектр тем, включно з математичним аналізом, теорією чисел, теорією груп та іншими основними галузями математики. Це переконливий доказ того, що ШІ може працювати з глибоким, багатокроковим міркуванням із гарантіями коректності — тією ж технологією, яку ми використовуємо для перевірки реального програмного забезпечення, апаратного забезпечення та наукових відкриттів, що потребують формальної логіки.