Di sini saya menyajikan formalisasi otomatis lengkap dari makalah matematika baru-baru ini (lagi!) Barańczuk, Stefan. "Mengurangi Jumlah Persamaan Mendefinisikan Subset dari n-Space di atas Medan Terbatas." Annales de la Faculté des sciences de Toulouse : Mathématiques, ser. 6, vol. 33, no. 1 (2024): 177–182. Saya menghabiskan beberapa hari untuk proyek ini. Pertama, saya menjalankan Aristoteles dengan @HarmonicMath , yang dalam waktu sekitar 15 jam benar-benar memformalkan pembuktian secara otomatis. Kemudian, dengan bantuan hebat dari @PietroMonticone, saya berhasil menyiapkan versi cetak biru dari bukti. Ini adalah versi di mana semua bagian dokumentasi di LaTeX menjadi interaktif dan dapat diperiksa dan dipelajari. Kita dapat melihat ketergantungan dalam bukti dan mempelajari hubungannya. Pada tahap pasca-pemrosesan, saya juga menggunakan Grok Heavy dan Codex CLI dengan GPT-5.2 dalam mode xhigh untuk menulis analisis baris demi baris dari bukti formal. Ini sangat membantu bagi orang-orang yang bukan programmer Lean 4 profesional. Anda benar-benar dapat menginternalisasi semua langkah pembuktian. Saya ingin merangkum kesan saya dan apa yang saya pelajari dari pengalaman ini. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei