Autoformalisering med Aristoteles genom @HarmonicMath och bakåtingenjörsarbete med @OpenAI GPT Codex CLI (egentligen GPT-5.2 med xhigh och alla experimentella perks aktiverade). Genom att arbeta på en övning från Bourbakis Algebra om matriser fick jag nästan 900 rader fullständigt dokumenterad Lean 4-kod, inklusive alla detaljer i beviset. Jag passerade sedan den – med en lämpligt designad agentisk uppsättning – till Codex CLI för att reverse-engineera motsvarande LaTeX-fil, och rekonstruerade bevisstegen direkt från Lean, i stil med Leslie Lamports strukturerade bevis. Detta är ännu inte Langlands-programmet, men vi behöver att denna typ av matematik på mellannivå automatiseras. Och det här händer nu. Jag byggde helt enkelt rätt agentisk setup, pipelineade allt och skrapade texten från Bourbaki (även den delen fungerade bra med @grok 4.1 vilket är häftigt för att förhandsgranska LaTeX live). Jag kommer att slutföra dokumentationen och lägga upp den på GitHub. Kolla beroendegrafen – Aristoteles hanterade allt själv. Och beviset är helt interaktivt. Vi lever i vetenskapens framtid nu!

I detta community-inlägg vill jag lägga upp länkar till några mycket engagerande spel och interaktiva miljöer (fritt tillgängliga) som hjälper människor att utforska högtravande koncept inom både programmering och matematik. Om du känner till någon annan rolig plats att besöka, posta bara nedan. Ha det så kul! Lutning: En samling mycket engagerande programmeringspussel som hjälper dig att lära dig hur matematik bevisas och formaliseras. Du kommer aldrig längre att se hårdheten hos 5*7=7*5 på samma sätt. NandGame: Du bygger din egen processor från grunden (även NAND är tillverkad av enklare kretsar). Mycket beroendeframkallande och superroligt! Kvantflugfälla: Det är här du äntligen kommer att få en förståelse för kvantberäkningar. Färgstark, gränslös, engagerande och matematiskt mycket djup. Scratch: Lär dig programmering på det roliga sättet. Euclidea: Lär dig hur man utför konstruktioner med linjal och kompass. Det brukade vara en del av skolans utbildning men nu är det en app. Roligt och mycket informativt. Planaritet: Försök hitta en grafinbäddning som visar att den faktiskt är plan. Oj då: Den ultimata cellulära automatautforskaren. Om du vill gräva djupare: SageMath: Det är ett kraftfullt datoralgebrasystem med Python-syntax. Det är idealiskt för kurser och syntaxen i SageMath ligger mycket närmare vanlig matematisk diskurs. Jag gillar att undervisa kurser med SageMath. GeoGebra: Du kan göra bevis, beräkningar och interaktiva applets. Det är ett roligt sätt att lära sig många olika aspekter av undegraduate-matematik. Wolfram-demonstrationsprojekt: En samling matematiska applets som kan hjälpa dig att förstå mycket avancerade ämnen. Du behöver inte Mathematica för att köra men du behöver det för att designa dina egna applets. Bevisets mekanik (av Heather Macbeth): Det är en bok med ett interaktivt GitHub-repo där du kan lära dig mer omfattande strukturen och syntaxen i Lean. En illustrerad talteori (av Martin H. Weissman): Detta är en lärobok om elementär talteori med tillämpningar. Och dessa applikationer finns tillgängliga på webbplatsen som en samling gratis Jupyter Notebooks som lär dig de viktigaste begreppen. Grafisk linjär algebra: På ett illustrerat och till viss del interaktivt sätt att lära sig djupa koncept i algebra. HomotopyContinuation.jl: Detta är ett otroligt vackert och interaktivt (med Julia) sätt att lära sig några mycket komplexa idéer från algebraisk geometri (sammanhängande komponenter, homotopifortsättningsmetoden) och med tillämpningar på mycket speciella algebraiska system som kommer från tillämpningar. Du kan lära dig Julia på vägen. Mathamaze: Det är en upplevelse av Helena Verrill. Vacker geometri, kakel, mönster. Helt enkelt underbart. Svårt att förklara: N: Ninjaernas väg: Om du tycker att matematik är svårt. Lär dig tålamodet på det hårda sättet. Varning: mycket beroendeframkallande HyperRogue: Du kan lära dig hyperbolisk geometri i en rogue-like-miljö.

Här presenterar jag en fullständig autoformalisering av en nyligen publicerad matematikuppsats (igen!) Barańczuk, Stefan. "Reducerar antalet ekvationer som definierar en delmängd av n-rummet över ett ändligt fält." Annales de la Faculté des sciences de Toulouse: Mathématiques, serie 6, vol. 33, nr 1 (2024): 177–182. Jag har lagt några dagar på det här projektet. Först körde jag Aristoteles av @HarmonicMath , som på ungefär 15 timmar helt autoformaliserade beviset. Sedan, med stor hjälp av @PietroMonticone, lyckades jag sätta upp en ritningsversion av beviset. Detta är en version där alla delar av dokumentationen i LaTeX blir interaktiva och kan granskas och studeras. Vi kan se beroendena i beviset och studera deras relationer. I efterbearbetningsfasen använde jag också Grok Heavy och Codex CLI med GPT-5.2 i xhigh-läge för att skriva en rad-för-rad-analys av det formella beviset. Detta är till stor hjälp för personer som inte är professionella Lean 4-programmerare. Du kan verkligen internalisera alla bevisens steg. Jag vill sammanfatta mina intryck och vad jag lärde mig av denna erfarenhet. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei