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