Matematiksel makaleler resmi doğrulamaya ihtiyaç duyar. Bu genellikle bir hakem tarafından gayri resmi olarak yapılır. Ama ya hakemin rolünün tanım ve teoremlerin formülasyonlarının titizlikle kontrol edilmesiyle sınırlı kalacağı Lean 4'e otomatik formalizasyon gibi daha sağlam bir şeye güvenebilseydik ne olurdu? Otomatik olarak oluşturulan kodun derlenmesi bir kanıt sertifikası haline gelir. Bu, @HarmonicMath'a kadar Aristoteles ile yaptığım uzun bir dönemde olan şey. Blueprint kurulumunda yardımcı olan @PietroMonticone ve @llllvvuu'a teşekkürler. Burada, arkadaşım Stefan Barańczuk'un Chebyshev bölünebilirlik dizileriyle ilgili bir makalesinin tam ve doğru otoformalizasyonunu sunuyorum. Kod yaklaşık 5000 satırlık oldukça önemsiz olmayan Lean'den oluşuyor. Ana makaledeki tüm tutarsızlıkları ve boşlukları düzeltiyor (hatta bazı devredilen önermeleri kanıtlıyor). Matematikin bazı alanlarında, temel sayı teorisi, kombinatorik ve analiz (Mathlib'in kapsadığı her türlü alan) dahil olmak üzere bazı matematik alanlarında kanıtların geçerliliği belgelenmesinde büyük bir değişime çok uzak olmadığımızı kanıtlayacağım. Bence bu yıl çok yoğun geçecek!