Formalisasi otomatis dengan Aristoteles dengan @HarmonicMath dan rekayasa balik dengan @OpenAI GPT Codex CLI (sebenarnya GPT-5.2 dengan xhigh dan semua fasilitas eksperimental diaktifkan). Mengerjakan latihan dari Aljabar Bourbaki tentang matriks, saya memperoleh hampir 900 baris kode Lean 4 yang didokumentasikan sepenuhnya, termasuk semua detail pembuktian. Saya kemudian meneruskannya-menggunakan pengaturan agen yang dirancang dengan tepat-ke Codex CLI untuk merekayasa balik file LaTeX yang sesuai, merekonstruksi langkah-langkah bukti langsung dari Lean, dalam gaya bukti terstruktur Leslie Lamport. Ini belum menjadi program Langlands, tetapi kita membutuhkan matematika tingkat menengah semacam ini untuk diotomatisasi. Dan ini terjadi sekarang. Saya hanya membangun pengaturan agen yang tepat, menyalurkan semuanya, dan mengikis teks dari Bourbaki (bahkan bagian itu bekerja dengan baik dengan @grok 4.1 yang keren untuk pratinjau LaTeX secara langsung). Saya akan menyelesaikan dokumentasi dan mempostingnya di GitHub. Periksa grafik dependensi-Aristoteles menangani semuanya dengan sendirinya. Dan buktinya sepenuhnya interaktif. Kita hidup di masa depan sains sekarang!

Dalam posting komunitas ini saya ingin menempatkan tautan ke beberapa game yang sangat menarik dan lingkungan interaktif (tersedia secara gratis) yang membantu orang mengeksplorasi konsep alis tinggi baik dalam pemrograman maupun matematika. Jika Anda mengetahui tempat menyenangkan lainnya untuk dikunjungi, cukup posting di bawah ini. Selamat bersenang-senang! Bersandar: Kumpulan teka-teki pemrograman yang sangat menarik yang membantu Anda mempelajari bagaimana matematika dibuktikan dan diformalkan. Anda tidak akan pernah melihat dengan cara yang sama kekerasan 5*7=7*5 lagi. Permainan Nand: Anda membuat prosesor Anda sendiri dari awal (bahkan NAND terbuat dari sirkuit yang lebih sederhana). Sangat adiktif dan sangat menyenangkan! Perangkap Lalat Kuantum: Di sinilah Anda akhirnya akan mendapatkan pemahaman tentang komputasi kuantum. Berwarna-warni, tanpa batas, menarik, dan secara matematis sangat dalam. Goresan: Pelajari pemrograman dengan cara yang menyenangkan. Euclidea: Pelajari cara melakukan konstruksi dengan penggaris dan kompas. Dulu itu adalah bagian dari pendidikan sekolah tetapi sekarang menjadi aplikasi. Menyenangkan dan sangat informatif. Planaritas: Cobalah untuk menemukan penyematan grafik yang menunjukkan bahwa itu memang planar. Astaga: Penjelajah automata seluler terbaik. Jika Anda ingin menggali lebih dalam: SageMath: Ini adalah sistem aljabar komputer yang kuat dengan sintaks Python. Ini ideal untuk kursus dan sintaks SageMath jauh lebih dekat dengan wacana matematika biasa. Saya suka mengajar kursus dengan SageMath. GeoGebra: Anda dapat melakukan pembuktian, perhitungan, dan applet interatif. Ini adalah cara yang menyenangkan untuk mempelajari berbagai aspek matematika yang belum lulus. Proyek Demonstrasi Wolfram: Kumpulan applet matematika yang dapat membantu Anda memahami topik yang sangat canggih. Anda tidak memerlukan Mathematica untuk berjalan tetapi Anda membutuhkannya untuk mendesain applet Anda sendiri. Mekanisme Pembuktian (oleh Heather Macbeth): Ini adalah buku dengan repositori GitHub interaktif di mana Anda dapat mempelajari struktur dan sintaks Lean secara lebih komprehensif. Teori Bilangan Bergambar (oleh Martin H. Weissman): Ini adalah buku teks tentang teori bilangan dasar dengan aplikasi. Dan aplikasi ini tersedia dari situs web sebagai kumpulan Jupyter Notebook gratis yang mengajarkan Anda konsep kunci. Aljabar Linear Grafis: Dalam ilustrasi dan sampai batas tertentu cara interaktif untuk mempelajari konsep mendalam dalam aljabar. HomotopyContinuation.jl: Ini adalah cara yang sangat indah dan interaktif (dengan Julia) untuk mempelajari beberapa ide yang sangat kompleks dari geometri aljabar (komponen terhubung, metode kelanjutan homotopi) dan dengan aplikasi ke sistem aljabar yang sangat khusus yang berasal dari aplikasi. Anda dapat mempelajari Julia di jalan. Mathamaze: Ini adalah pengalaman oleh Helena Verrill. Geometri yang indah, ubin, pola. Sungguh luar biasa. Sulit untuk dijelaskan: N: Cara Ninja: Jika menurut Anda matematika itu sulit. Pelajari kesabaran dengan cara yang sulit. Peringatan: sangat membuat ketagihan HyperRogue: Anda dapat mempelajari geometri hiperbolik di lingkungan seperti nakal.

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