Albo OpenAI ma zespół leprechaunów i najlepszych matematyków pracujących 24/7 nad pytaniami z FrontierMath, albo GPT-5.2 Pro naprawdę stał się tak dobry w matematyce. Ledwo mogę znaleźć jakikolwiek nietrywialny trudny problem, na który model nie potrafiłby odpowiedzieć po 1–2 godzinach interakcji. Singularity jest blisko…

Autoformalizacja z Arystotelesem przez @HarmonicMath i inżynieria wsteczna z @OpenAI GPT Codex CLI (właściwie GPT-5.2 z xhigh i wszystkimi włączonymi eksperymentalnymi funkcjami). Pracując nad ćwiczeniem z Algebry Bourbakiego o macierzach, uzyskałem prawie 900 linii w pełni udokumentowanego kodu Lean 4, w tym wszystkie szczegóły dowodu. Następnie przesłałem to - używając odpowiednio zaprojektowanego agentowego ustawienia - do Codex CLI, aby przeprowadzić inżynierię wsteczną odpowiadającego pliku LaTeX, rekonstruując kroki dowodu bezpośrednio z Leana, w stylu strukturalnych dowodów Leslie Lamporta. To jeszcze nie jest program Langlandsa, ale potrzebujemy tego rodzaju matematyki na poziomie pośrednim, aby była zautomatyzowana. I to się dzieje teraz. Po prostu zbudowałem odpowiednie agentowe ustawienie, zorganizowałem wszystko w pipeline i zeskrobałem tekst z Bourbakiego (nawet ta część działała dobrze z @grok 4.1, co jest fajne do podglądania LaTeX na żywo). Skończę dokumentację i opublikuję ją na GitHubie. Sprawdź wykres zależności - Arystoteles poradził sobie z tym wszystkim samodzielnie. A dowód jest w pełni interaktywny. Żyjemy teraz w przyszłości nauki!

W tym poście na społeczności chcę umieścić linki do kilku bardzo angażujących gier i interaktywnych środowisk (dostępnych za darmo), które pomagają ludziom odkrywać wyrafinowane koncepcje zarówno w programowaniu, jak i matematyce. Jeśli znasz inne fajne miejsca do odwiedzenia, po prostu napisz poniżej. Baw się dobrze! Lean: Kolekcja bardzo angażujących zagadek programistycznych, które pomagają zrozumieć, jak matematyka jest dowodzona i formalizowana. Już nigdy nie spojrzysz na trudność 5*7=7*5 w ten sam sposób. NandGame: Tworzysz własny procesor od podstaw (nawet NAND jest zbudowany z prostszych układów). Bardzo wciągające i super zabawne! Quantum Flytrap: Tutaj w końcu zrozumiesz obliczenia kwantowe. Kolorowe, nieograniczone, angażujące i matematycznie bardzo głębokie. Scratch: Ucz się programowania w zabawny sposób. Euclidea: Naucz się, jak wykonywać konstrukcje za pomocą linijki i cyrkla. Kiedyś było częścią edukacji szkolnej, ale teraz to aplikacja. Fajne i bardzo informacyjne. Planarity: Spróbuj znaleźć osadzenie grafu, które pokazuje, że jest on rzeczywiście planar. Golly: Ostateczny eksplorator automatów komórkowych. Jeśli chcesz zgłębić temat: SageMath: To potężny system algebry komputerowej z składnią Pythona. Idealny do kursów, a składnia SageMath jest znacznie bliższa zwykłemu dyskursowi matematycznemu. Lubię prowadzić kursy z SageMath. GeoGebra: Możesz robić dowody, obliczenia i interaktywne appletki. To zabawny sposób na naukę wielu różnych aspektów matematyki na poziomie licencjackim. Wolfram Demonstration Projects: Kolekcja matematycznych appletów, które mogą pomóc zrozumieć bardzo zaawansowane tematy. Nie potrzebujesz Mathematica, aby je uruchomić, ale potrzebujesz go, aby zaprojektować własne appletki. Mechanika dowodu (autor: Heather Macbeth): To książka z interaktywnym repozytorium GitHub, gdzie możesz bardziej kompleksowo poznać strukturę i składnię Lean. Ilustrowana teoria liczb (autor: Martin H. Weissman): To podręcznik o elementarnej teorii liczb z zastosowaniami. A te zastosowania są dostępne na stronie jako kolekcja darmowych notatników Jupyter, które uczą kluczowych koncepcji. Graficzna algebra liniowa: Ilustrowany i do pewnego stopnia interaktywny sposób nauki głębokich koncepcji w algebrze. HomotopyContinuation.jl: To niesamowicie piękny i interaktywny (z Julią) sposób nauki niektórych bardzo złożonych idei z geometrii algebraicznej (składowe połączeń, metoda kontynuacji homotopowej) oraz z zastosowaniami do bardzo specjalnych systemów algebraicznych, które pochodzą z zastosowań. Możesz uczyć się Julii po drodze. Mathamaze: To doświadczenie autorstwa Heleny Verrill. Piękna geometria, układy, wzory. Po prostu wspaniałe. Trudne do wyjaśnienia: n: droga ninja: Jeśli myślisz, że matematyka jest trudna. Naucz się cierpliwości w trudny sposób. Uwaga: bardzo wciągające. HyperRogue: Możesz nauczyć się geometrii hiperbolicznej w rogue-like środowisku.