Auto-formalizzazione con Aristotele da @HarmonicMath e reverse engineering con @OpenAI GPT Codex CLI (in realtà GPT-5.2 con xhigh e tutti i vantaggi sperimentali abilitati). Lavorando su un esercizio dell'Algebra di Bourbaki riguardante le matrici, ho ottenuto quasi 900 righe di codice Lean 4 completamente documentato, inclusi tutti i dettagli della dimostrazione. Poi l'ho passato - utilizzando un setup agentico progettato appositamente - a Codex CLI per reverse-engineering del corrispondente file LaTeX, ricostruendo i passaggi della dimostrazione direttamente da Lean, nello stile delle dimostrazioni strutturate di Leslie Lamport. Questo non è ancora il programma di Langlands, ma abbiamo bisogno che questo tipo di matematica a livello intermedio venga automatizzato. E questo sta accadendo ora. Ho semplicemente costruito il giusto setup agentico, canalizzato tutto e estratto il testo da Bourbaki (anche quella parte ha funzionato bene con @grok 4.1, che è fantastico per visualizzare LaTeX in tempo reale). Finirò la documentazione e la pubblicherò su GitHub. Controlla il grafo delle dipendenze - Aristotele ha gestito tutto da solo. E la dimostrazione è completamente interattiva. Stiamo vivendo nel futuro della scienza ora!

In questo post della comunità voglio mettere link a alcuni giochi altamente coinvolgenti e ambienti interattivi (disponibili gratuitamente) che aiutano le persone a esplorare concetti elevati sia nella programmazione che nella matematica. Se conosci altri posti divertenti da visitare, semplicemente posta qui sotto. Divertiti! Lean: Una raccolta di puzzle di programmazione altamente coinvolgenti che ti aiutano a imparare come la matematica viene provata e formalizzata. Non guarderai mai più la difficoltà di 5*7=7*5 nello stesso modo. NandGame: Crea il tuo processore da zero (anche il NAND è fatto di circuiti più semplici). Estremamente avvincente e super divertente! Quantum Flytrap: Qui finalmente otterrai una comprensione dei calcoli quantistici. Colorato, illimitato, coinvolgente e matematicamente molto profondo. Scratch: Impara a programmare in modo divertente. Euclidea: Impara a eseguire costruzioni con righello e compasso. Era parte dell'educazione scolastica ma ora è un'app. Divertente e molto informativa. Planarity: Cerca di trovare un'incorporazione del grafo che dimostri che è effettivamente planare. Golly: L'esploratore definitivo degli automi cellulari. Se vuoi approfondire: SageMath: È un potente sistema di algebra computazionale con sintassi Python. È ideale per corsi e la sintassi di SageMath è molto più vicina al discorso matematico regolare. Mi piace insegnare corsi con SageMath. GeoGebra: Puoi fare dimostrazioni, calcoli e applet interattive. È un modo divertente per apprendere molte diverse sfaccettature della matematica universitaria. Wolfram Demonstration Projects: Una raccolta di applet matematiche che possono aiutarti a comprendere argomenti molto sofisticati. Non hai bisogno di Mathematica per eseguire, ma ne hai bisogno per progettare le tue applet. The Mechanics of Proof (di Heather Macbeth): È un libro con un repo interattivo su GitHub dove puoi apprendere in modo più completo la struttura e la sintassi di Lean. An Illustrated Theory of Numbers (di Martin H. Weissman): Questo è un libro di testo sulla teoria dei numeri elementari con applicazioni. E queste applicazioni sono disponibili dal sito web come una raccolta di Jupyter Notebooks gratuiti che ti insegnano i concetti chiave. Graphical Linear Algebra: In modo illustrato e in una certa misura interattivo per apprendere concetti profondi in algebra. HomotopyContinuation.jl: Questo è un modo incredibilmente bello e interattivo (con Julia) di apprendere alcune idee altamente complesse dalla geometria algebrica (componenti connesse, metodo di continuazione omotopica) e con applicazioni a sistemi algebrici molto speciali che derivano da applicazioni. Puoi imparare Julia lungo il percorso. Mathamaze: È un'esperienza di Helena Verrill. Geometria bellissima, piastrelle, modelli. Semplicemente meraviglioso. Difficile da spiegare: n: la via del ninja: Se pensi che la matematica sia difficile. Impara la pazienza nel modo difficile. Attenzione: altamente avvincente. HyperRogue: Puoi imparare la geometria iperbolica in un ambiente rogue-like.

Qui presento una completa auto-formalizzazione di un recente articolo di matematica (di nuovo!) Barańczuk, Stefan. "Ridurre il numero di equazioni che definiscono un sottoinsieme dello spazio n su un campo finito." Annales de la Faculté des sciences de Toulouse : Mathématiques, ser. 6, vol. 33, no. 1 (2024): 177–182. Ho trascorso alcuni giorni su questo progetto. Prima, ho eseguito Aristotle di @HarmonicMath, che in circa 15 ore ha completamente auto-formalizzato la dimostrazione. Poi, con l'ottimo aiuto di @PietroMonticone, sono riuscito a impostare una versione blueprint della dimostrazione. Questa è una versione in cui tutte le parti della documentazione in LaTeX diventano interattive e possono essere ispezionate e studiate. Possiamo vedere le dipendenze nella dimostrazione e studiare le loro relazioni. Nella fase di post-elaborazione, ho anche utilizzato Grok Heavy e Codex CLI con GPT-5.2 in modalità xhigh per scrivere un'analisi riga per riga della dimostrazione formale. Questo è un grande aiuto per le persone che non sono programmatori professionisti di Lean 4. Puoi davvero interiorizzare tutti i passaggi della dimostrazione. Voglio riassumere le mie impressioni e ciò che ho imparato da questa esperienza. @vladtenev @Leonard41111588 @HarmonicMath @llllvvuu @littmath @AlexKontorovich @jdlichtman @KenOno691 @CarinaLHong @gdb @hongyuan_mei