Enten har OpenAI et team av nisser og toppmatematikere som jobber døgnet rundt med FrontierMath-spørsmål, eller så har GPT-5.2 Pro faktisk blitt så god i matematikk. Jeg finner knapt noe ikke-trivielt vanskelig problem som modellen ikke kan svare på etter 1–2 timers interaksjon. Singulariteten er nær...

Autoformalisering med Aristoteles ved @HarmonicMath og reversering med @OpenAI GPT Codex CLI (egentlig GPT-5.2 med xhigh og alle eksperimentelle fordeler aktivert). Da jeg jobbet med en øvelse fra Bourbakis Algebra om matriser, fikk jeg nesten 900 linjer med fullstendig dokumentert Lean 4-kode, inkludert alle detaljene i beviset. Deretter sendte jeg den – med et passende designet agentisk oppsett – til Codex CLI for å reversere den tilsvarende LaTeX-filen, og rekonstruerte bevistrinnene direkte fra Lean, i stil med Leslie Lamports strukturerte bevis. Dette er ikke Langlands-programmet ennå, men vi trenger at denne typen matematikk på mellomnivå automatiseres. Og dette skjer nå. Jeg bygde rett og slett riktig agentisk oppsett, pipelinet alt, og skrapet teksten fra Bourbaki (selv den delen fungerte bra med @grok 4.1, noe som er kult for forhåndsvisning av LaTeX live). Jeg skal fullføre dokumentasjonen og legge den ut på GitHub. Sjekk avhengighetsgrafen – Aristoteles håndterte alt selv. Og beviset er fullt interaktivt. Vi lever i vitenskapens fremtid nå!

I dette fellesskapsinnlegget ønsker jeg å legge ut lenker til noen svært engasjerende spill og interaktive miljøer (fritt tilgjengelige) som hjelper folk å utforske høykulturelle konsepter innen både programmering og matematikk. Hvis du kjenner til et annet morsomt sted å besøke, er det bare å poste nedenfor. Ha det gøy! Lean: En samling svært engasjerende programmeringspuslespill som hjelper deg å lære hvordan matematikk bevises og formaliseres. Du vil aldri se hardheten til 5*7=7*5 på samme måte lenger. NandGame: Du lager din egen prosessor fra bunnen av (selv NAND er laget av enklere kretser). Svært vanedannende og supermorsomt! Kvantefluefanger: Det er her du endelig vil få en forståelse av kvanteberegningene. Fargerikt, grenseløst, engasjerende og matematisk veldig dypt. Scratch: Lær programmering på den morsomme måten. Euclidea: Lær hvordan du utfører konstruksjoner med linjal og kompass. Det pleide å være en del av skoleundervisningen, men nå er det en app. Morsomt og veldig informativt. Planaritet: Prøv å finne en graf-embedding som viser at den faktisk er plan. Herregud: Den ultimate utforskeren av cellulære automater. Hvis du vil grave dypere: SageMatematikk: Det er et kraftig dataalgebrasystem med Python-syntaks. Det er ideelt for kurs, og syntaksen i SageMath er mye nærmere vanlig matematisk diskurs. Jeg liker å undervise i kurs med SageMath. GeoGebra: Du kan gjøre bevis, beregninger og interaktive appleter. Det er en morsom måte å lære mange forskjellige sider av undegraduate-matematikk på. Wolfram-demonstrasjonsprosjekter: En samling matematiske applets som kan hjelpe deg å forstå svært avanserte emner. Du trenger ikke Mathematica for å kjøre, men du trenger det for å designe dine egne applets. Bevisets mekanikk (av Heather Macbeth): Det er en bok med et interaktivt GitHub-repo hvor du kan lære mer omfattende strukturen og syntaksen til Lean. En illustrert tallteori (av Martin H. Weissman): Dette er en lærebok om elementær tallteori med anvendelser. Og disse applikasjonene er tilgjengelige på nettsiden som en samling gratis Jupyter-notatbøker som lærer deg nøkkelkonseptene. Grafisk lineær algebra: På en illustrert og til en viss grad interaktiv måte å lære dype konsepter i algebra. HomotopyContinuation.jl: Dette er en utrolig vakker og interaktiv (med Julia) måte å lære noen svært komplekse ideer fra algebraisk geometri (sammenhengende komponenter, homotopi-fortsettelsesmetoden) og med anvendelser på helt spesielle algebraiske systemer som kommer fra applikasjoner. Du kan lære Julia på veien. Mathamaze: Det er en opplevelse av Helena Verrill. Vakker geometri, flislegginger, mønstre. Rett og slett fantastisk. Vanskelig å forklare: n: Ninjaens vei: Hvis du synes matematikk er vanskelig. Lær tålmodigheten på den harde måten. Advarsel: svært avhengighetsskapende HyperRogue: Du kan lære hyperbolsk geometri i et rogue-like-miljø.