Dieci progressi nella matematica e nell'informatica teorica

Vogliamo offrire a scienziati e matematici strumenti che accelerino le scoperte. Per questo abbiamo recentemente annunciato ChatGPT per la ricerca accademica⁠, un'iniziativa che offre a 100.000 scienziati e matematici l'accesso gratuito ai nostri migliori modelli ChatGPT. Continuiamo inoltre a valutare i nostri modelli su problemi di ricerca aperti durante lo sviluppo.

A maggio abbiamo presentato una confutazione generata dall'IA⁠ della congettura delle distanze unitarie di Erdős, scoperta durante la valutazione di un modello non ancora pubblicato. Questo lavoro ha già ispirato ulteriori sviluppi nella matematica e nell'informatica teorica¹. Oggi presentiamo una selezione di dieci risultati, ciascuno dei quali risolve un problema aperto da tempo o compie progressi sostanziali verso la sua soluzione. Questi problemi riguardano la geometria in dimensione elevata, la teoria dei codici, la complessità dei circuiti aritmetici, la teoria dei gruppi, le algebre di operatori, la complessità quantistica, la crittografia su reticoli e la combinatoria estremale. Tutti questi problemi rivestono notevole interesse per le rispettive comunità matematiche, e diversi sono di ampio interesse per la matematica nel suo complesso.

Presentiamo nuovi risultati per i seguenti problemi. I risultati sono stati ottenuti da una versione interna di Astra, il nostro prossimo modello di punta. Il numero totale di token necessari per trovare le soluzioni a questi problemi avrebbe un costo di circa 2.000 dollari alle tariffe dell'API Sol. Queste argomentazioni sono state poi trasformate in manoscritti da persone che si sono avvalse dello stesso modello. Successivamente, il modello ha formalizzato ogni argomentazione in un certificato Lean⁠(si apre in una nuova finestra). Per ogni soluzione pubblichiamo inoltre il resoconto del processo di pensiero del modello.

1. Impacchettamento di sfere in dimensione elevata. Nuovi limiti superiori per la densità dell'impacchettamento di sfere fino alla soglia di Cohn–Elkies.
2. Codici binari e sferici: limiti migliorati esponenzialmente per la dimensione massima dei codici binari con una qualsiasi distanza minima prestabilita, con risultati analoghi per i codici sferici in dimensione elevata.
3. Gruppi non sofic. Una costruzione che dimostra l'esistenza di gruppi non sofic, affrontando una questione aperta centrale nella teoria dei gruppi.
4. Congettura di rigidità di Connes. Confutazione di una congettura di lunga data secondo cui determinati gruppi sarebbero univocamente determinati dalle loro algebre di von Neumann.
5. Complessità dei circuiti aritmetici. Nuovi limiti inferiori per il calcolo del permanente mediante circuiti e formule aritmetiche, tra cui un limite inferiore di ordine n⁴/log n per le formule aritmetiche.
6. Ripetizione parallela quantistica. Un teorema di ripetizione parallela esponenziale per giochi quantistici generali a due giocatori, che estende un principio fondamentale della teoria classica della complessità.
7. Problema del vettore più vicino. Difficoltà di approssimazione entro un fattore polinomiale per il problema del vettore più vicino, una questione fondamentale sui reticoli legata alla crittografia post-quantistica.
8. Congettura del volume di Ehrhart. Determinazione, in ogni dimensione, del massimo volume possibile di un corpo convesso il cui centroide sia il suo unico punto reticolare interno.
9. Numeri di Ramsey multicolore. Un limite inferiore superesponenziale per i numeri di Ramsey multicolore dei triangoli, che risolve il problema 183 di Erdős.
10. Congetture sui numeri estremali. Risultati sulle congetture di compattezza e degenerazione nella teoria estremale dei grafi, che risolvono i problemi 146 e 180 di Erdős.

La comparsa di sistemi capaci di contribuire alla ricerca matematica solleva interrogativi a cui un'azienda tecnologica non può rispondere da sola. Esistono molte opinioni sul ruolo dell'IA nella matematica. Nutriamo profondo rispetto e comprensione per chi è preoccupato dal suo impatto, compresi i firmatari della Dichiarazione di Leida sull'IA e la matematica⁠(si apre in una nuova finestra). Riteniamo che l'attribuzione debba rispecchiare onestamente il modo in cui è stato prodotto un risultato: attribuire a esseri umani la paternità di una dimostrazione generata interamente da un sistema di IA traviserebbe sia il contributo del sistema sia la natura dell'autentico lavoro intellettuale umano. Abbiamo contribuito alla preparazione dei manoscritti e alla formalizzazione delle dimostrazioni in Lean e ci assumiamo la responsabilità della loro correttezza, mentre le argomentazioni matematiche sono state generate dal nostro sistema. Ci auguriamo che la comunità matematica esamini a fondo questi risultati, li collochi nel loro contesto e dia vita alle idee su cui si fondano attraverso nuove ricerche e scoperte.

Con l'evoluzione dei sistemi di IA in collaboratori di ricerca sempre più sofisticati, garantire un accesso diffuso è fondamentale per sostenere scienziati e matematici mentre esplorano e definiscono il futuro delle proprie discipline in questa fase di trasformazione.