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

Makalah matematika membutuhkan validasi formal. Ini biasanya dilakukan secara informal oleh wasit. Tetapi bagaimana jika kita dapat mengandalkan sesuatu yang lebih kuat seperti formalisasi otomatis menjadi Lean 4 di mana peran wasit akan direduksi menjadi pemeriksaan yang cermat terhadap formulasi definisi dan teorema? Kompilasi kode yang dihasilkan secara otomatis akan menjadi sertifikat bukti. Inilah yang terjadi dalam jangka panjang yang saya lakukan dengan Aristoteles pada tahun @HarmonicMath. Terima kasih kepada @PietroMonticone dan @llllvvuu karena telah membantu pengaturan cetak biru. Di sini saya menyajikan formalisasi otomatis yang benar dari makalah teman saya Stefan Barańczuk tentang urutan perpecahan Chebyshev. Kodenya adalah sekitar 5000 baris Lean yang sangat tidak sepele. Ini mengoreksi semua inkonsistensi dan celah dalam makalah utama (bahkan membuktikan beberapa proposisi yang didelegasikan). Saya akan memposting serangkaian eksperimen semacam itu, membuktikan bahwa dalam beberapa bidang matematika, termasuk teori bilangan dasar, kombinatorika dan analisis (segala macam hal yang dicakup oleh Mathlib) kita tidak jauh dari pergeseran besar-besaran dalam dokumentasi validitas pembuktian. Saya pikir ini akan menjadi tahun yang sibuk!

Jika saya seorang siswa hari ini, berinteraksi dengan LLM canggih akan terasa hampir seperti kecurangan. Pagi ini saya secara acak mengambil gambar papan tulis dan meminta ChatGPT-5.2-Pro untuk menjelaskan konteksnya, solusinya, dan beberapa komentar sampingan tentang teorema Chevalley yang terkenal pada set yang dapat dikonstruksi. Apa yang saya terima adalah laporan yang sangat mendalam, mensintesis materi berkualitas tinggi tentang geometri aljabar yang diambil dari seluruh internet. Ini menimbulkan pertanyaan serius: apa upaya dan tantangan sebenarnya bagi siswa saat ini? Biaya tentu saja merupakan salah satu faktor, tetapi begitu akses ke model-model ini tersedia, bagaimana seseorang harus belajar di tanah kelimpahan ini, di mana penjelasan, referensi, dan eksplorasi interaktif semuanya dapat diakses secara instan? Mungkin perjuangan bukan lagi tentang memperoleh informasi atau bahkan memahami argumen individu, tetapi tentang mengembangkan penilaian: mengetahui pertanyaan mana yang harus diajukan, penjelasan mana yang harus dipercaya, bagaimana mengenali kedalaman versus kemungkinan permukaan, dan bagaimana menginternalisasi ide daripada hanya mengkonsumsinya. Dalam lingkungan di mana jawaban berlimpah, kesulitan sebenarnya mungkin terletak pada pembentukan rasa, intuisi matematis, dan kapasitas untuk menavigasi - daripada tenggelam dalam - pengetahuan yang tiba-tiba berlebih.