Cerca

AlphaProof Nexus risolve 9 problemi aperti, Claude Code Auto Mode su Pro, Copilot Eclipse open source

AlphaProof Nexus risolve 9 problemi aperti, Claude Code Auto Mode su Pro, Copilot Eclipse open source

ai-powered-markdown-translator

Articolo tradotto dal fr all’it con gpt-5.4-mini.

Vedi progetto su GitHub ↗

Questa settimana, Google DeepMind compie un salto nella ricerca matematica con AlphaProof Nexus, un agente in grado di risolvere problemi aperti da diversi decenni. Sul fronte di Anthropic, la modalità auto di Claude Code si apre al piano Pro e integra Sonnet 4.6. GitHub open source il plugin Copilot per Eclipse, e Alibaba attiva la cache implicita su Qwen3.7-Max.


AlphaProof Nexus — Un agente IA risolve problemi matematici aperti da decenni

25 maggio 2026 — Google DeepMind ha annunciato AlphaProof Nexus, un framework agentico (agentic framework) per la ricerca di dimostrazioni formali alimentato da Gemini, accompagnato da un articolo sottomesso ad arXiv il 21 maggio (arXiv:2605.22763).

L’agente si basa su un ciclo che alterna generazione tramite Gemini e verifica formale tramite il linguaggio di dimostrazione Lean. Questa combinazione garantisce il rigore matematico delle dimostrazioni prodotte: il LLM propone, Lean convalida o rifiuta, e l’agente itera.

Risultati pubblicati:

DominioRisultatiContesto
Problemi aperti di Erdős9 risolti su 353 valutatiDi cui 2 aperti da 56 anni
Congetture OEIS44 risolte su 492Online Encyclopedia of Integer Sequences
Geometria algebrica1 problema aperto risoltoAperto da 15 anni
Ottimizzazione min-max1 domanda aperta risoltaAperta da 7 anni

Il costo per problema risolto è di poche centinaia di dollari — un ordine di grandezza che illustra l’efficienza economica dell’approccio agentico per la ricerca matematica formale.

AlphaProof Nexus è già distribuito in collaborazione con matematici in diversi ambiti: combinatoria, teoria dei grafi, geometria algebrica e ottica quantistica. Questo lavoro si inserisce nella continuità di AlphaProof (2024), che mirava a problemi di livello olimpico. AlphaProof Nexus punta a problemi aperti di ricerca, segnando una tappa verso l’uso dell’IA come strumento autonomo di scoperta matematica.

“AI agents are advancing research-level math.”

🇮🇹 Gli agenti IA fanno progredire la matematica al livello della ricerca.Pushmeet Kohli, VP Research, Google DeepMind su X

🔗 Articolo arXiv 2605.22763


Claude Code v2.1.149 — Dettaglio /usage per categoria e 25+ correzioni

23 maggio 2026 — È stata pubblicata la versione 2.1.149 di Claude Code, concretizzando la funzionalità /usage breakdown per categoria annunciata da Boris Cherny la settimana precedente.

FunzionalitàDettaglio
/usage breakdownDettaglio dei consumi per categoria: skills, sous-agenti, plugin, server MCP
/diff navigationNavigazione da tastiera: frecce, j/k, PgUp/PgDn, Home/End
GFM task listsCaselle di spunta Markdown ([ ] / [x]) visualizzate correttamente
EnterpriseNuovo parametro gestito allowAllClaudeAIMcps per managed-mcp.json

La release corregge anche una ventina di bug: aggiramento delle autorizzazioni PowerShell in cd, esaurimento della tabella vnode su macOS con find, blocco della finestra di dialogo managed-settings, modifiche fantasma in /config, crash di /insights su campi opzionali mancanti, e spinner di riflessione che rimane arancione tra le chiamate agli strumenti.

La versione 2.1.150, pubblicata lo stesso giorno, apporta solo miglioramenti infrastrutturali interni senza cambiamenti visibili.

🔗 Changelog Claude Code


Claude Code Auto Mode — Disponibile su Pro, Sonnet 4.6 integrato

23 maggio 2026 — Anthropic annuncia due estensioni della modalità auto di Claude Code:

“Two updates to auto mode: · Now available on the Pro plan · Sonnet 4.6 is now supported, alongside Opus 4.7. Shift+tab, and let Claude run.”

🇮🇹 Due aggiornamenti della modalità auto: ora disponibile sul piano Pro; Sonnet 4.6 è supportato, insieme a Opus 4.7. Shift+tab, e lascia che Claude lavori.@ClaudeDevs su X

La modalità auto, attivata tramite Shift+Tab, consente a Claude di eseguire azioni in modo autonomo senza convalida manuale a ogni passaggio. Finora riservata ai piani superiori, è ora accessibile agli abbonati Pro. L’aggiunta di Sonnet 4.6 offre un’opzione più economica di Opus 4.7 per le sessioni lunghe, riducendo il consumo di crediti in modalità autonoma.

Per accedere a questi cambiamenti: claude update oppure aggiornamento dell’app desktop Claude. L’annuncio ha generato 1,18 milioni di visualizzazioni su X.


GitHub Copilot for Eclipse — Open source sotto licenza MIT

21 maggio 2026 — GitHub ha reso open source il plugin GitHub Copilot per Eclipse, disponibile su GitHub sotto licenza MIT all’indirizzo github.com/microsoft/copilot-for-eclipse.

L’insieme delle funzionalità è esposto per contributi della comunità:

FunzionalitàStato
Code completion (completamenti inline)Open source
Next Edit Suggestions (NES)Open source
Chat (flusso di conversazione, chiamate agli strumenti)Open source
Agent mode (workflow agentici multistep)Open source
Skills e prompt filesOpen source
BYOK (Bring Your Own Key)Open source
Agenti personalizzati, sous-agenti, piano agent, MCPOpen source

La motivazione è la trasparenza e l’innovazione della comunità nello spirito dell’ecosistema aperto di Eclipse. Contributi sono già stati ricevuti dalla comunità fin dall’apertura.

🔗 Annuncio GitHub Changelog


Qwen3.7-Max — Cache implicita attivata in produzione

25 maggio 2026 — Alibaba attiva la cache implicita (implicit caching) su Qwen3.7-Max, il suo modello di punta orientato agli agenti.

La cache si attiva automaticamente per tutte le richieste API — nessuna modifica al codice richiesta. Gli sviluppatori beneficiano immediatamente di richieste più rapide e meno costose sui contesti ripetitivi. Per tassi di cache più elevati e deterministici, Alibaba raccomanda la cache esplicita, documentata su Alibaba Cloud.

🔗 Tweet @Alibaba_Qwen


Brevi

  • MiniMax Hailuo AI all’AIFF di Hong Kong (HKUST) — Il 2° AI Film Festival organizzato dall’HKUST ha ricevuto 1.300 candidature da 80 paesi. Hailuo AI vi era rappresentato accanto a Tencent e Z.ai durante un panel sulla democratizzazione del cinema IA. 🔗 minimax.io

  • NVIDIA DGX Spark — 16 agenti IA locali simultanei — Dimostrazione della comunità ritwittata da @NVIDIAAI: 2x DGX Spark (GB10) + MiniMax M2.7 NVFP4 fanno girare 16 agenti IA in streaming simultaneo, senza API cloud. 🔗 @NVIDIAAI su X


Cosa significa

Una svolta per la ricerca matematica formale. AlphaProof Nexus segna una rottura: l’IA non si limita più a problemi da competizione o a benchmark accademici, ma si confronta con problemi aperti che i matematici non sono riusciti a risolvere per decenni. La combinazione Gemini + Lean crea un ciclo di verifica formale che garantisce che le dimostrazioni siano corrette, non solo plausibili. Il costo di poche centinaia di dollari per problema risolto suggerisce che questo approccio sta diventando accessibile ai laboratori di ricerca, non solo ai giganti del settore.

La maturità dell’outillage agentico dal lato Anthropic. L’arrivo della modalità auto sul piano Pro e l’integrazione di Sonnet 4.6 segnalano che Anthropic considera l’uso agentico autonomo sufficientemente stabile per il grande pubblico. La versione 2.1.149, con il suo breakdown /usage per categoria, risponde a un’esigenza concreta degli sviluppatori che costruiscono sistemi multi-agente complessi: capire con precisione cosa consuma il loro budget per ottimizzare le loro architetture.

Apertura vs sovranità software. L’open source di Copilot per Eclipse sotto MIT e l’attivazione della cache implicita su Qwen3.7-Max illustrano due strategie diverse per conquistare gli sviluppatori. GitHub punta sulla trasparenza e sull’ecosistema Eclipse per ampliare l’adozione di Copilot negli ambienti Java aziendali. Alibaba punta sulla riduzione automatica dei costi senza attriti per rendere Qwen3.7-Max più competitivo rispetto alle alternative cloud.

L’industrializzazione dei media generativi progredisce. La partecipazione di MiniMax all’AIFF di Hong Kong — 1.300 candidature da 80 paesi — e la dimostrazione NVIDIA di 16 agenti locali simultanei su DGX Spark delineano un ecosistema in cui la creazione video tramite IA penetra nei workflow professionali del cinema, sia in festival sia nell’infrastruttura locale.


Fonti