Burada yakın zamanda yazılmış bir matematik makalesinin tam otomatik resmileştirilmesini sunuyorum (yine!) Barańczuk, Stefan. "N-uzayın bir alt kümesini sonlu bir alan üzerinde tanımlayan denklem sayısının azaltılması." Annales de la Faculté des Sciences de Toulouse: Mathématiques, seri 6, cilt 33, sayı 1 (2024): 177–182. Bu proje üzerinde birkaç gün harcadım. Öncelikle, Aristoteles'i @HarmonicMath ile çalıştırdım ve yaklaşık 15 saatte kanıtı tamamen otomatik olarak formalize ettim. Sonra, @PietroMonticone'ın büyük yardımıyla kanıtın bir taslak versiyonunu kurmayı başardım. Bu, LaTeX'teki tüm dokümantasyon bölümlerinin etkileşimli hale geldiği ve incelenip incelenebilen bir versiyondur. Kanıtta bağımlılıkları görebilir ve ilişkilerini inceleyebiliriz. Sonradan işleme aşamasında, Grok Heavy ve Codex CLI'yi GPT-5.2 ile xhigh modunda kullanarak resmi kanıtın satır satır analizini yazdım. Bu, profesyonel Lean 4 programcısı olmayanlar için harika bir yardım. Kanıtın tüm adımlarını gerçekten içselleştirebilirsiniz. İzlenimlerimi ve bu deneyimden öğrendiklerimi özetlemek istiyorum. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei

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!

Bugün bir öğrenci olsaydım, son teknoloji LLM'lerle etkileşimde bulunmak neredeyse hile yapmak gibi gelirdi. Bu sabah rastgele tahtanın bir fotoğrafını çektim ve ChatGPT-5.2-Pro'dan yapılanabilir kümeler üzerine ünlü Chevalley teoremi hakkında bağlamı, çözümü ve bazı yan yorumları açıklamasını istedim. Aldığım rapor, internetin çeşitli yerlerinden cebirsel geometri üzerine yüksek kaliteli materyalleri sentezleyen son derece derin bir rapordu. Bu ciddi bir soruyu gündeme getiriyor: bugün öğrenciler için gerçek çaba ve zorluk nedir? Maliyet kesinlikle bir faktör, ancak bu modellere erişim sağlandığında, açıklamalar, referanslar ve etkileşimli keşiflerin anında erişilebilir olduğu bu bolluk diyarında nasıl öğrenilmelidir? Belki de mücadele artık bilgi edinmek ya da bireysel argümanları anlamak değil, yargı geliştirmekle ilgilidir: hangi soruların sorulacağını, hangi açıklamalara güvenileceğini bilmek, derinlik ile yüzeysel olasılığı nasıl tanıyacağımızı ve fikirleri sadece tüketmek yerine içselleştirmeyi bilmek. Cevapların bolca olduğu bir ortamda, gerçek zorluk zevk, matematiksel sezgi ve bu ani bilgi fazlasında boğulmak yerine yol alma yeteneği oluşturmakta olabilir.