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

I documenti matematici necessitano di una validazione formale. Questo di solito viene fatto informalmente da un revisore. Ma cosa succederebbe se potessimo fare affidamento su qualcosa di più robusto come l'auto-formalizzazione in Lean 4, dove il ruolo del revisore sarebbe ridotto a un controllo meticoloso delle formulazioni delle definizioni e dei teoremi? La compilazione del codice generato automaticamente diventerebbe un certificato di prova. Questo è ciò che è accaduto in un progetto più lungo che ho fatto con Aristotele da @HarmonicMath. Grazie a @PietroMonticone e @llllvvuu per aver aiutato con la configurazione del progetto. Qui presento un'auto-formalizzazione completa e corretta di un articolo del mio amico Stefan Barańczuk riguardo alle sequenze di divisibilità di Chebyshev. Il codice è di circa 5000 righe di Lean altamente non banale. Corregge tutte le incoerenze e le lacune nel documento principale (inclusa la dimostrazione di alcune proposizioni delegate). Pubblicherò una serie di esperimenti di questo tipo, dimostrando che in alcune aree della matematica, inclusa la teoria dei numeri elementare, la combinatoria e l'analisi (tutte le cose coperte da Mathlib), non siamo lontani da un cambiamento massiccio nella documentazione della validità delle prove. Penso che quest'anno sarà frenetico!