Ho personalmente superato un limite e sono un po' in soggezione. Questa è la mia prima prova completamente automatizzata, generata da LLM e auto-formalizzata di un nuovo teorema matematico. Lasciami impostare il problema: abbiamo tre cerchi rotanti con sei posizioni ciascuno, tutti e tre che si intersecano in un totale di sei punti. Prova che il gruppo di movimenti che generano è il gruppo simmetrico completo S_{12}. Questo è un problema che ho notato originariamente in un delizioso puzzle nel gioco Machinarium di Amanita Design. Il compito non è estremamente difficile, ma apparentemente ha due prove: 1. Una ricerca esaustiva sulle classi di coniugazione per rappresentare tutte le trasposizioni (l'ho fatto molti anni fa ma non l'ho mai pubblicato). 2. Una prova generata da LLM (in questo caso prodotta circa tre mesi fa da GPT-5-Pro), o in realtà due prove, entrambe utilizzando in modo brillante un teorema di Jordan sui gruppi primitivi (o una variante strettamente correlata che è ancora più diretta). ( Quello che mi mancava fino a stasera era uno strumento per auto-formalizzare questa prova. Grazie a @HarmonicMath, ho avuto accesso al loro straordinario software, Aristotele. In sintesi, ecco cosa ho fatto: A. Ho generato automaticamente la prova con un LLM (e l'ho eseguita più volte per ottenere una versione molto migliorata). B. Ho ridotto la prova al testo matematico essenziale—definizioni, proposizioni, lemmi, teoremi—con prove fornite dall'LLM. C. Ho eseguito il sistema Aristotele durante la notte (via API). Questa mattina ho ricevuto una versione completamente formalizzata in Lean (circa 700 righe di codice). Il codice si compila, quindi ora ho un certificato che conferma che la prova generata dall'LLM ha effettivamente portato a una soluzione corretta. Inoltre, ho ottenuto una prova concettuale, migliore della mia brute-force. Ho intenzione di spingerla ulteriormente a una classe più ampia di tali problemi algebrici. È un piccolo progetto, ma per me segna un traguardo. Ora ho strumenti che, con la mia orchestrazione, possono davvero aiutarmi a scoprire, formalizzare e studiare le prove dei teoremi matematici. Questo non è banale. Domande: 1. Come si scalerà questo in futuro? 2. Quanta formazione sarà necessaria per avere successo in tali compiti? 3. Come dovremmo trattare la paternità di tali prove? 4. Qual è il ruolo più profondo dei matematici?

Qualcuno ha intenzione di partecipare? Sarà molto divertente!

Uno dei motivi per cui non vedo l'ora di vedere nuove architetture è che i problemi nella topologia algebrica richiedono fondamentalmente intuizioni che vanno ben oltre semplici manipolazioni simboliche. Spesso è molto più facile presentare uno schizzo visivo di un argomento basato su isotopia/omotopia piuttosto che progettare formule precise e renderlo completamente formale. Spero che una combinazione di modelli del mondo, manipolazione simbolica e rappresentazioni della dinamica degli oggetti sia un percorso verso architetture completamente nuove. Ne abbiamo bisogno se vogliamo risolvere problemi matematici difficili che vanno oltre il semplice testo. Nell'immagine (basata su arXiv: 2107.01664) puoi vedere quanto sia facile intuire il paradosso delle manette ma quanto sarebbe difficile scriverlo formalmente con formule.