🚀 Aleph kanıtlayıcısı CANAVAR moduna geçti 20+ yıldır çözülmemiş 4 matematik problemi. Lean 4'te formal ispatlar. 48 saatten az. Toplamda 5 bin doların altında. ✅ Binom kuyruk sınırları varsayımı (Telgarsky, 2009) ✅ Kuantum kapı kafes yaklaşımı (Greene & Damelin, 2015)* ✅ Erdős 124 ✅ Erdős 481 ✅ PutnamBench liderlik tablosunda #1 Yapay zeka matematiğinin dönemi geldi. Bu süreci hayata 🙏 geçirmelerine yardımcı oldukları için @BorisHanin ve @ylecun'e özel teşekkürler Ve @LeanFRO ekibine büyük tebrikler — bunların hiçbiri sizin oluşturduğunuz inanılmaz temel olmadan mümkün değil. Aleph yakında halka açık olacak, takipte kalın! *Sardari (2015) sonuçlarına bağlı olarak, resmileştirme beklemektedir

Aleph kanıtlayıcı ajanımız, PutnamBench'te #1 oldu; bu, Putnam problemlerinden oluşan bir kıstala - en zor üniversite düzeyindeki matematik olimpiyatlarından biri - tamamen makine kontrolüyle yapılan kanıtlarla ve insan müdahalesi olmadan formalize edilmiş. Putnam problemleri genellikle IMO problemlerinden daha zor kabul edilir ve kalkülüs, sayı teorisi, grup teorisi ve matematiğin diğer temel alanları gibi geniş bir konu yelpazesini kapsar. Bu, yapay zekanın derin, çok adımlı akıl yürütmeyi doğruluk garantileriyle yönetebileceğinin güçlü bir kanıtıdır — gerçek yazılım, donanım ve bilimsel keşifleri doğrulamak için kullandığımız aynı teknoloji ve resmi mantık gerektiriyor.