🚀 Aleph prover только что включил РЕЖИМ ЗВЕРЯ 4 математические задачи, неразрешенные более 20 лет. Формальные доказательства в Lean 4. Менее 48 часов. Менее 5 тысяч долларов в общей сложности. ✅ Гипотеза о биномиальных хвостах (Телгарский, 2009) ✅ Приближение квантных ворот в решетке (Грин и Дамелин, 2015)* ✅ Эрдёш 124 ✅ Эрдёш 481 ✅ #1 на лидерборде PutnamBench Эра математики ИИ наступила. Особая благодарность @BorisHanin и @ylecun за помощь в реализации этого 🙏 И огромные поздравления команде @LeanFRO — ничего из этого было бы невозможно без невероятного фундамента, который вы построили. Aleph скоро будет доступен для публики, следите за новостями! *условно по результатам Сардара (2015), формализация в ожидании