Tech News, powered by Quinck. Una nuova puntata discussa davanti alla telecamera: il video è sul nostro canale, e lo trovi qui sotto.
▶ Guarda la puntata su YouTube
Questa volta le notizie sono due, più una domanda che le tiene insieme. Il 6 ottobre OpenAI ha pubblicato centinaia di risultati matematici nuovi, molti certificati da una prova formale. Nella stessa settimana un team minuscolo ha messo su GitHub cloni open source di Photoshop, Premiere, Word, Excel e AutoCAD, scritti con un agente AI, mentre i social si riempivano di Minecraft dentro Elden Ring.
Sembrano storie lontane. La domanda in mezzo, perché l'AI è così brava proprio in matematica, mostra che non lo sono: l'AI diventa fortissima dove la risposta si può verificare in automatico. Una dimostrazione in Lean passa il controllo oppure no. Un clone di Photoshop produce lo stesso output dell'originale oppure no. Un gioco decompilato si ricompila identico byte per byte, oppure no.
In 30 secondi
- OpenAI ha pubblicato una repository con centinaia di paper matematici: soluzioni o avanzamenti parziali importanti per circa 370 famiglie di risultati, circa il 40% con una prova in Lean allegata, ottenuti in media con 3 ore di calcolo a problema. I problemi sottoposti erano circa 4.000, e tre risultati sono già stati ritirati.
- L'AI eccelle in matematica per via del reinforcement learning, in particolare dell'RLVR: il modello impara dove la risposta si può controllare in automatico. Per questo la medicina, dove la verifica passa da esperimenti reali, avanza più lentamente.
- Lo stesso principio sta rifacendo il software. Le app di ArtCraft clonano mezza Creative Cloud, Office e AutoCAD in una settimana, con Claude Opus 5.5 e Rust. Nei videogiochi esplodono mashup e decompilazioni guidate dall'AI. La domanda legale, e quella di mercato, sono entrambe aperte.
1. OpenAI pubblica centinaia di risultati matematici
Il 6 ottobre OpenAI ha pubblicato su GitHub una repository con centinaia di paper matematici: risoluzioni, o avanzamenti parziali importanti, per circa 370 famiglie di risultati. Una buona parte, circa il 40%, ha allegata una prova in Lean, il proof assistant che verifica automaticamente una dimostrazione: se passa il controllo, è corretta, e non serve fidarsi di nessuno.
I risultati arrivano da un modello interno, non ancora rilasciato al pubblico. È lo stesso che poco più di un mese fa ha portato alla soluzione del problema di Navier-Stokes.
Tempi e costi: 3 ore di calcolo a problema
L'obiezione più ovvia riguarda i soldi. La prova su Navier-Stokes, secondo alcune stime, è costata milioni di dollari, con migliaia di agenti al lavoro in parallelo. Con quella cifra si paga un bel po' di ricercatori.
Può darsi che un team umano ben finanziato sarebbe arrivato a risultati simili, anche se il controfattuale non lo avremo mai. Ma ci sono due differenze. La prima è il tempo: per gli umani sarebbero stati anni. La seconda pesa di più: la stragrande maggioranza di questi nuovi risultati è uscita con circa 3 ore di calcolo in media.
Due precisazioni, doverose:
- I problemi sottoposti erano circa 4.000. Quelli risolti sono una quota significativa, ma lontana dal totale.
- Quelli senza certificato Lean potrebbero contenere errori. Tre sono già stati ritirati.
Solo controesempi? Le obiezioni
Si sente dire spesso che l'AI risolve sempre allo stesso modo: trova un controesempio a forza bruta e chiude lì, senza nulla dell'ingegno che associamo a un matematico.
Le obiezioni sono due. Anche quando la soluzione è un controesempio, come per la congettura Jacobiana risolta in precedenza da Anthropic o per Navier-Stokes, il percorso per arrivarci quasi mai è banale: non è una ricerca cieca nello spazio delle soluzioni. E per i risultati di ottobre l'obiezione proprio non regge: molti non sono controesempi, ma costruzioni complesse che i matematici che le stanno esaminando trovano poco intuitive.
Per qualche anno si è potuto sostenere che gli LLM non ragionassero davvero. Era una posizione dibattuta ma difendibile. I sistemi di oggi sono un'altra cosa: il ragionamento logico c'è, e in alcuni domini va già oltre quello umano.
Come la stanno prendendo i matematici
Male, in parte. Sui social si trovano dottorandi e ricercatori che scoprono che il problema su cui lavoravano da anni è stato risolto da un giorno all'altro. E la domanda che circola è brutale: se il valore degli esseri umani non sta più nel trovare soluzioni, cosa resta?
Per ora, almeno due cose.
Capire. I paper scritti dall'AI, per non parlare delle prove in Lean, sono difficilissimi da leggere. Serve qualcuno, aiutato dagli LLM, che digerisca questa mole di risultati e trovi le spiegazioni intuitive. Sapere che una proposizione è vera non vuol dire capirla, ed è la comprensione profonda che fa nascere nuove domande e nuovi rami di ricerca.
Scegliere la direzione. Anche i modelli più recenti non mostrano grande creatività nel decidere cosa studiare. Per adesso sono gli umani a scegliere su quali problemi puntarli. Domani potrebbe cambiare.
Il nostro take: il matematico non è una calcolatrice
Ridurre il lavoro del matematico alla produzione di soluzioni è come ridurre quello di un ingegnere alla scrittura di righe di codice. La soluzione è l'output misurabile, ma il valore sta nel capire perché funziona e nel sapere quale domanda fare dopo. Su questo l'AI per ora aiuta, ma non sostituisce.
Resta il fatto che questo gruppo di pubblicazioni è un risultato storico, un punto di svolta. Proprio per questo serve una conversazione seria e pragmatica sul ruolo che vogliamo dare all'essere umano nella matematica.
2. Perché l'AI è così brava in matematica?
Facciamo un passo indietro. Perché i laboratori AI investono così tanto sulla matematica, invece che su problemi con un impatto immediato come la medicina?
Detta così sembra un paradosso. Avrebbero tutto l'interesse a farlo: un risultato in medicina porterebbe più investimenti e una reputazione molto migliore. Il punto è che oggi non possono, per limiti concreti che dipendono dalla natura stessa di quei campi.
Un'intelligenza diversa dalla nostra
L'intuizione naturale è che un'AI capace di risolvere problemi aperti da decenni in matematica debba cavarsela altrettanto bene altrove. Il passaggio non è affatto automatico.
La prima cosa da interiorizzare è che l'intelligenza di questi sistemi è profondamente diversa dalla nostra, e che bisogna liberarsi, anche se costa fatica, degli assunti che ci portiamo dietro dall'intelligenza umana. Un modello può essere fortissimo in un campo e fallire miseramente in un compito che a noi sembra banale. Negli esseri umani le capacità sono molto più livellate tra un dominio e l'altro.
Per capire perché la matematica sta da una parte di questo divario, bisogna guardare da dove arriva buona parte dei progressi recenti: il reinforcement learning.
Reinforcement learning e RLVR
È vero che gli LLM sono allenati a predire il prossimo token, ma è metà della storia. Quella fase si chiama pre-training: il modello elabora quantità enormi di testi di ogni tipo e impara a prevedere cosa viene dopo.
Poi c'è il post-training, che pesa sempre di più, e lì dentro c'è il reinforcement learning. Qui l'obiettivo cambia: non si tratta più di predire, ma di arrivare alla risposta giusta. Il modello propone una soluzione, la soluzione viene valutata, e il modello viene premiato oppure no.
In una variante specifica, l'RLVR (reinforcement learning from verifiable rewards), la valutazione è automatica. Servono due ingredienti: grandi quantità di problemi dello stesso tipo, e un modo per controllare in automatico se la risposta è corretta. La parola chiave è verificabilità.
Il limite del mondo reale: perché non la medicina
Da qui si capisce dove aspettarsi i progressi: in tutte le discipline dove una risposta si verifica con un calcolo. Un esempio quotidiano sono i dati strutturati. Oggi un LLM restituisce un output strutturato con altissima precisione, se glielo si chiede: la struttura è verificabile, ed è molto probabile che le aziende AI abbiano ambienti di reinforcement learning dedicati proprio a questo.
Il rovescio è che i problemi che richiedono interazione con il mondo esterno sono molto meno attaccabili. Per un farmaco nuovo o una nuova terapia non bastano ragionamento e verifica computazionale: servono esperimenti reali. Lì i progressi saranno più lenti e limitati, almeno per ora. Il limite è chiaro a tutti, e diversi team ci stanno lavorando da più direzioni.
La matematica è il caso perfetto: con un proof assistant come Lean una dimostrazione si controlla interamente via calcolo, senza toccare il mondo esterno. Ed è lo stesso principio che spiega la terza notizia.
3. L'AI ha imparato a rifare il software (e i videogiochi)
Photoshop rifatto in una settimana: le app di ArtCraft
Tra il 30 settembre e il 7 ottobre il team di ArtCraft ha pubblicato su GitHub un'intera famiglia di applicazioni gratuite e open source:
- PhotoCraft per Photoshop, VectorCraft per Illustrator, FilmCraft per Premiere, LightCraft per Lightroom, EffectCraft per After Effects, DesignCraft per InDesign, più un clone di Acrobat;
- WordCraft, GridCraft e DeckCraft per Word, Excel e PowerPoint;
- CADCraft per AutoCAD e SoundCraft per Pro Tools.
Dietro non c'è una big tech, ma uno sviluppatore, Brandon Thomas, con un team piccolissimo. Ha usato Claude Opus 5.5 e ha scritto tutto in Rust, con una versione WebAssembly che gira nel browser. Nella maggior parte dei commit Claude compare come co-autore. La reazione è stata entusiasta: PhotoCraft ha superato le 20.000 stelle su GitHub in circa una settimana.
Perché proprio Adobe
Per sua stessa ammissione, a Thomas la goccia l'ha data la penale di disdetta. Il tema è caldo: nel 2024 il governo statunitense aveva fatto causa ad Adobe proprio sulle penali e sulla difficoltà di cancellare l'abbonamento, e la vicenda si è chiusa con un accordo da 150 milioni di dollari. Adobe nega ogni illecito.
Come si clona un software senza il suo codice
Secondo il team, il codice dei vendor non è mai stato toccato. Il README parla di un'implementazione basata solo su specifiche pubbliche e comportamento osservato. È reverse engineering black box:
- gli agenti studiano documentazione, formati di file, screenshot e tutorial;
- spezzano il programma in componenti (livelli, pennelli, filtri);
- generano il codice per ogni pezzo;
- confrontano l'output con quello del Photoshop vero, e se non coincide ricominciano.
Per i file PSD esiste una specifica pubblicata da Adobe, la stessa strada percorsa da Photopea o Pixelmator. Per CADCraft è più complicato, perché il formato DWG non ha una specifica aperta: il team usa una libreria di terze parti, acadrust (licenza MPL-2.0), e scrive nero su bianco di non avere alcun legame con Autodesk.
I decompilatori guidati dall'AI
I decompilatori con l'AI però esistono. Progetti come GhidraMCP o Reverse Engineer Anything collegano gli agenti a Ghidra, IDA o Hopper, e l'agente può ispezionare un'app compilata e ricostruirla. Per ArtCraft, finora, nessuno ha mostrato prove che sia stato usato il codice dei vendor.
Quanto funzionano davvero
Sono versioni alpha, e il team lo dice apertamente. Secondo la roadmap, PhotoCraft copre oggi il 25-35% di quello che serve a un professionista per lavorare tutti i giorni, e chi l'ha provata parla di bug e strumenti imprevedibili. Thomas promette la parità di funzioni entro un mese: un obiettivo decisamente ottimista.
Perché l'AI è così brava a farlo
Il reverse engineering esiste da quarant'anni. Cosa è cambiato adesso?
È il discorso della matematica, applicato al software. Il reverse engineering è un problema verificabile per eccellenza: produci un'ipotesi, la compili, la esegui e la confronti con l'originale. O torna, o no. Lo stesso ciclo di prova e verifica, ma automatizzato e in parallelo su centinaia di funzioni.
Prima una clean room seria richiedeva due team separati, avvocati e mesi o anni di lavoro. Oggi quel costo è crollato di ordini di grandezza.
Videogiochi rifatti e mescolati
La stessa ondata ha investito i videogiochi, a partire da fine settembre. Il primo caso virale è il progetto di Chasm del 19 settembre: Skate 3 riscritto in Rust, poi la fisica dello skate dentro Call of Duty: Modern Warfare 2. Da lì è esploso tutto: Mario in Elden Ring, Spider-Man che volteggia per Gotham, Mario Kart negli Zombies di Call of Duty, Minecraft dentro Elden Ring.
Le tecniche sono due:
- sovrapposizione: i due giochi girano in contemporanea e i personaggi di uno vengono sovrapposti all'altro, una specie di green screen evoluto ma con gli input collegati. Tiri con l'arco in Minecraft, e Steve tira con l'arco in Elden Ring;
- decompilazione e ricostruzione: i giochi vengono decompilati e ricostruiti in un motore moderno, come Bevy in Rust, incollando sistemi nati incompatibili come scheletri e animazioni.
L'AI pesa molto, ma sopra un enorme lavoro umano. Chasm descrive il suo progetto come quasi interamente vibe-coded, però si appoggia su anni di reverse engineering fatto a mano da altri, e per la parte Minecraft ha speso settimane di tuning manuale.
Decompilazioni e giochi portati su PC
Fuori dai mashup c'è tutta la scena delle decompilazioni e dei port per PC:
- la decompilazione di Super Smash Bros. Melee è arrivata al 100% il 7 settembre, dopo più di sei anni, con l'AI che ha accelerato l'ultimo tratto;
- quella di Snowboard Kids è passata da quasi due anni di lavoro a 84 giorni;
- Fable 2 è stato fatto girare su PC in circa un'ora;
- c'è chi ha bruciato oltre 500 miliardi di token in tre mesi per decompilare un intero FPS in C++.
Anche qui conta la verificabilità, in pieno. Nelle matching decompilation il compilatore produce un binario identico byte per byte all'originale, oppure no. Le risposte sbagliate si scartano da sole.
Le reazioni dei modder
Non tutti hanno applaudito. Il Discord di N64 Recomp non mostra né supporta progetti vibe-coded, alcuni port si presentano apposta come "100% scritti da umani", e qualche modder storico minaccia di smettere se questa roba diventa la norma.
Ma è legale?
Dipende da cosa si usa come input. Il copyright protegge il codice per come è scritto, non quello che il codice fa.
In Europa la Corte di Giustizia l'ha detto chiaramente nel 2012, con la sentenza SAS Institute contro World Programming: funzionalità, linguaggio di programmazione e formati di file non sono protetti. La direttiva sul software, all'articolo 5(3), dà il diritto di osservare, studiare e testare un programma, e le clausole contrattuali che lo vietano sono nulle.
Sulla decompilazione il margine è più stretto: l'articolo 6 la consente solo per l'interoperabilità, solo per le parti necessarie e mai per costruire un programma sostanzialmente simile. Negli Stati Uniti ci sono precedenti favorevoli, Sega contro Accolade (1992) e Google contro Oracle (2021), ma i tribunali hanno anche fatto valere le clausole anti reverse engineering contro chi aveva accettato la licenza.
L'AI aggiunge un problema nuovo. La clean room classica funziona perché si dimostra che chi ha scritto il codice non ha mai visto l'originale. Ma un modello addestrato su mezzo internet potrebbe averlo visto nei dati di training. Il caso scuola è il leak del codice di Claude Code del 31 marzo: in pochi giorni sono comparse reimplementazioni "clean room" fatte con l'AI, e se valgano davvero come tali è una domanda ancora aperta. C'è anche il rovescio: negli Stati Uniti un'opera generata interamente dall'AI non è proteggibile, quindi anche il clone potrebbe ritrovarsi senza copyright.
Licenze e brevetti: i vendor sono disarmati?
Le licenze provano a chiudere la porta. Le condizioni d'uso di Adobe, alla sezione 17, considerano reverse engineering anche il monitoraggio di input e output di un'app per ricrearla. Microsoft vieta di usare i suoi prodotti per replicarne le funzionalità, Autodesk vieta reverse engineering e decompilazione salvo dove la legge lo consente. Il limite è che un contratto vincola solo chi l'ha accettato: se un team lavora da documenti pubblici e comportamenti descritti da altri, non è chiaro cosa il vendor possa fargli.
Disarmati però non sono. Restano i brevetti, che coprono un metodo comunque sia scritto il codice, e Adobe ne ha migliaia su funzioni software. Restano i marchi. Sono strade lente e pubbliche, ma esistono. E c'è il look and feel: il README di PhotoCraft si presenta dicendo che chi conosce Photoshop conosce già PhotoCraft, ed è lì che il rischio è più concreto.
Per i giochi il quadro è ancora meno favorevole: i publisher sono storicamente aggressivi. Take-Two aveva colpito con un DMCA il progetto re3 su GTA nel 2021, chiuso poi con un accordo nel 2023. Il video di Super Mario 64 dentro Elden Ring è già stato rimosso per una segnalazione di copyright. E molti mashup usano asset originali, che è il terreno più scivoloso.
Cosa cambia per chi vende software
Il codice smette di essere il fossato. Se il comportamento visibile di un'app si rifà in una settimana, il valore si sposta su ciò che codice non è: anni di file nei formati proprietari, servizi cloud dietro un account, ecosistemi di plugin, gestione delle identità, certificazioni, supporto. Nessuna delle app di ArtCraft fa girare i plugin di Photoshop o le macro VBA.
Rischia di più chi vive soprattutto di un'app desktop con un formato documentato: le app Adobe e i tool di disegno di Autodesk sono i più esposti. Microsoft 365 meno, perché è anche posta, Teams, SharePoint e identità: si può rifare l'editor, ma la piattaforma resta.
E per chi compra software
Per le aziende che comprano licenze, la novità è soprattutto leva negoziale. Anche senza migrare, un'alternativa testata su un gruppo di utenti leggeri cambia la trattativa al rinnovo.
Con qualche attenzione:
- installer fasulli con nomi famosi, il classico veicolo di malware quando un progetto diventa virale;
- nessuna manleva sulla proprietà intellettuale e nessun supporto;
- il rischio di pagare due volte, adottando il clone ma rinnovando comunque le licenze.
E per chi, come noi, sviluppa software su commessa, le facce sono due. Da un lato oggi si può ricostruire o modernizzare un gestionale legacy senza sorgenti in tempi impensabili fino a ieri. Dall'altro anche il proprio prodotto diventa replicabile: se il valore che si vende è solo l'interfaccia, qualcuno può rifarla guardandola girare.
Il filo rosso: dove la risposta si verifica, l'AI arriva
Tre storie, un solo meccanismo. L'AI non è uniformemente intelligente: è straordinariamente forte dove esiste un modo automatico per dire "giusto" o "sbagliato". La matematica con Lean, l'output di un'app confrontato con quello dell'originale, un binario che si ricompila identico. Dove la verifica passa dal mondo reale, come in medicina, il passo è molto più lento.
Per chi costruisce software le conseguenze pratiche sono tre.
Chiedersi quanto è verificabile quello che si costruisce. Più un compito ha un criterio automatico di successo, più in fretta l'AI lo saprà fare. Vale per le funzioni di un prodotto e per i processi interni: test, conversioni di formato, migrazioni di codice sono il terreno dove l'AI rende di più già oggi.
Spostare il valore oltre l'interfaccia. Se basta guardare un software girare per rifarlo, la difesa sono i dati, le integrazioni, il servizio e la fiducia. Il codice si copia, la fiducia no.
Non scambiare il risultato per la comprensione. Vale per i matematici e vale per il codice generato: una soluzione che nessuno sa spiegare funziona finché non cambia qualcosa. Il lavoro umano si sposta lì, nel capire e nello scegliere la prossima domanda.
Domande frequenti
Cosa ha pubblicato OpenAI il 6 ottobre 2026? Una repository GitHub con centinaia di paper matematici che contengono soluzioni, o avanzamenti parziali importanti, per circa 370 famiglie di risultati. Circa il 40% ha una prova in Lean allegata. Li ha prodotti un modello interno non ancora rilasciato, lo stesso usato per Navier-Stokes.
Cos'è Lean e perché conta? Lean è un proof assistant: un linguaggio formale in cui scrivere dimostrazioni matematiche che un programma verifica automaticamente. Se una prova in Lean passa il controllo è corretta, senza bisogno di fidarsi di chi l'ha scritta.
Quanto calcolo è servito per i risultati matematici di OpenAI? In media circa 3 ore per problema, per la grande maggioranza dei risultati. Su circa 4.000 problemi sottoposti ne è stata risolta una quota significativa ma lontana dal totale, e tre risultati senza certificato Lean sono già stati ritirati per errori.
L'AI risolve i problemi matematici solo trovando controesempi? No. Anche quando la soluzione è un controesempio il percorso per trovarlo raramente è banale, e molti dei risultati pubblicati da OpenAI sono costruzioni complesse che i matematici trovano poco intuitive.
Perché l'AI è così brava in matematica? Per il reinforcement learning, e in particolare l'RLVR (reinforcement learning from verifiable rewards): il modello viene premiato quando arriva alla risposta corretta, e in matematica la correttezza si può verificare in automatico. Più un dominio è verificabile, più in fretta l'AI migliora.
Perché l'AI non fa altrettanti progressi in medicina? Perché in medicina la verifica finale passa da esperimenti reali, non da un calcolo. Senza una verifica automatica e rapida il reinforcement learning ha molto meno margine, almeno per ora.
Cosa sono le app di ArtCraft? Cloni gratuiti e open source di Photoshop, Illustrator, Premiere, Lightroom, After Effects, InDesign, Acrobat, Word, Excel, PowerPoint, AutoCAD e Pro Tools, pubblicati su GitHub tra il 30 settembre e il 7 ottobre 2026. Li ha sviluppati Brandon Thomas con un piccolo team, usando Claude Opus 5.5 e Rust. Sono ancora in alpha.
Come si clona un software senza il suo codice sorgente? Con il reverse engineering black box: si studiano documentazione, formati di file e comportamento dell'app, la si divide in componenti, si genera il codice per ciascuno e si confronta l'output con quello dell'originale finché coincide.
È legale clonare un software con l'AI? Dipende dall'input. Il copyright protegge il codice, non le funzionalità: in Europa la sentenza SAS Institute del 2012 e la direttiva sul software consentono di osservare, studiare e testare un programma. La decompilazione è ammessa solo per l'interoperabilità. Restano brevetti, marchi, look and feel e le clausole di licenza per chi le ha accettate.
Cosa sono i mashup di videogiochi fatti con l'AI? Progetti che uniscono giochi diversi, come Minecraft in Elden Ring o la fisica di Skate 3 in Call of Duty, sovrapponendo due giochi in esecuzione con gli input collegati oppure decompilandoli e ricostruendoli in un motore moderno.
Cosa cambia per le aziende che vendono o comprano software? Per chi vende, il codice non è più una difesa: il valore si sposta su dati, integrazioni, servizi cloud, ecosistemi e supporto. Per chi compra, un'alternativa open source anche immatura diventa leva negoziale al rinnovo, con i rischi di installer fasulli, assenza di manleva e licenze pagate due volte.
Fonti
- OpenAI: repository openai/math
- OpenAI: annuncio della soluzione di Navier-Stokes
- Science: costi e controversia sul risultato
- NPR: costi e leggibilità dei risultati
- Dmitry Rybin: post su X
- Aran Nayebi: post su X
- Wikipedia: Reinforcement learning
- Wikipedia: Reasoning model
- arXiv: Tülu 3, il paper che introduce l'RLVR
- PetaPixel: le app Adobe ricostruite con l'AI
- HotHardware: Claude Opus 5.5 e Rust dietro i cloni
- TechSpot: le motivazioni e la causa del governo USA ad Adobe
- TweakTown: maturità delle app e brevetti
- daily.dev: il metodo black box
- MindStudio: i decompilatori guidati dall'AI
- Licenseware: quadro legale e impatti su vendor e clienti
- ToolScout: cronologia dei mashup di videogiochi
- VGC: mashup e reazioni dei modder
- MindStudio: mashup e decompilazione di Snowboard Kids
- Dot Esports: Melee, Fable 2 e N64 Recomp
- Maurice Heumann: 500 miliardi di token per decompilare un FPS
- Live in the Future: la clean room nell'era dell'AI
- Reed Smith: Clean room coding in the age of AI: who owns the code?
