Entah OpenAI memiliki tim leprechaun dan matematikawan top yang bekerja 24/7 pada pertanyaan FrontierMath, atau GPT-5.2 Pro benar-benar menjadi ahli matematika. Saya hampir tidak dapat menemukan masalah sulit yang tidak sepele yang tidak dapat dijawab oleh model setelah 1-2 jam interaksi. Singularitas sudah dekat...

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.