terence tao offre una ricompensa per il cervello più potente di internet! gli esseri umani con intelligenza artificiale sovvertono i problemi matematici? i netizen di versailles se ne sono andati
2024-09-29
한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina
nuovo rapporto sulla saggezza
redattore: enea così assonnato[introduzione alla nuova saggezza]recentemente, tao zhexuan ha lanciato una sfida alla maggior parte dei netizen e degli appassionati di matematica: possono gli appassionati di matematica più popolari, gli assistenti di dimostrazione, gli assistenti automatizzati e l’intelligenza artificiale unire le forze per dimostrare problemi matematici che si estendono per diversi ordini di grandezza?
vuoi partecipare al progetto di ricerca matematica "crowdsourcing" lanciato da terence tao?la ricerca matematica sulle prove assistita dall’intelligenza artificiale sta diventando sempre più fattibile
ognuno di loro ha abbastanza familiarità con gli aspetti del progetto per convalidare i rispettivi contributi.ma se si vogliono organizzare progetti di ricerca matematica su larga scala, soprattutto progetti che coinvolgono contributi pubblici, la cosa diventa molto più problematica.il motivo è che è difficile verificare il contributo di tutti.alla fine del 2023, terence tao ha annunciato che il progetto lean4, che ha formalizzato la dimostrazione della congettura del polinomio di freiman-ruzsa, ha avuto successo dopo tre settimane (l'immagine mostra lo stato più recente)tieni presente che un singolo errore in una parte di un argomento matematico può causare il fallimento dell'intero progetto.inoltre, data la complessità di un tipico progetto di matematica, non è realistico aspettarsi che membri del pubblico con una formazione universitaria in matematica diano contributi significativi.da ciò possiamo anche capire che anche l’integrazione degli strumenti di intelligenza artificiale nei progetti di ricerca matematica è estremamente impegnativa.poiché l’intelligenza artificiale può generare argomentazioni che sembrano ragionevoli ma in realtà non hanno senso, è necessaria un’ulteriore verifica prima che la parte generata dall’intelligenza artificiale possa essere aggiunta al progetto.fortunatamente, linguaggi assistiti da prove come lean offrono potenziali modi per superare questi ostacoli e consentire la collaborazione tra matematici professionisti, il pubblico in generale e strumenti di intelligenza artificiale.questo approccio si basa sulla premessa che i progetti possono essere suddivisi in modo modulare in parti più piccole che possono essere completate senza dover comprendere l’intero progetto.gli esempi attuali includono principalmente progetti che formalizzano risultati matematici esistenti (come la formalizzazione della congettura pfr recentemente dimostrata da marton).queste formalizzazioni vengono effettuate principalmente attraverso il crowdsourcing da parte di contributori umani (compresi matematici professionisti e membri del pubblico interessati).allo stesso tempo, ci sono anche alcuni tentativi emergenti di introdurre strumenti più automatizzati per completare l’attività, compresi i tradizionali dimostratori automatici di teoremi e strumenti più moderni basati sull’intelligenza artificiale.diventa possibile esplorare nuovi problemi matematici
e,terenzio taosi ritiene inoltre che questo nuovo paradigma possa essere utilizzato non solo per formalizzare la matematica esistente, ma anche per esplorare una matematica completamente nuova!in passato lui e il suo successore hanno organizzato un progetto di collaborazione online "polymath", che ne è un buon esempio.tuttavia, questo progetto non incorporava un linguaggio ausiliario di prova nel flusso di lavoro e i contributi dovevano essere gestiti e verificati da moderatori umani, il che richiedeva molto tempo e limitava l’ulteriore espansione di questi progetti.ora, tao zhexuan spera che l’aggiunta di un linguaggio ausiliario di prova possa rompere questo collo di bottiglia.è particolarmente interessato a sapere se sia possibile utilizzare questi strumenti moderni per esplorare una classe di problemi matematici simultaneamente, invece di concentrarsi solo su uno o due problemi alla volta.in sostanza, questo approccio è modulare per attività ripetitive e gli strumenti di crowdsourcing e automazione possono essere particolarmente utili se esiste una piattaforma per coordinare rigorosamente tutti i contributi.questo tipo di problema matematico non sarebbe stato scalabile utilizzando i metodi precedenti. a meno che non si esplori lentamente un punto dati alla volta con documenti individuali nel corso di molti anni finché non si ottiene un'intuizione ragionevole su questo tipo di problema.inoltre, disporre di un ampio set di dati sui problemi può aiutare a eseguire valutazioni delle prestazioni di vari strumenti di automazione e confrontare l'efficienza di diversi flussi di lavoro.nel luglio di quest'anno, il quinto numero di busy beaver è stato confermato essere 47.176.870.alcuni precedenti progetti informatici in crowdsourcing, come great internet mersenne prime search (gimps), sono simili nello spirito a questi progetti, sebbene utilizzino un meccanismo di prova di lavoro più tradizionale, piuttosto che dimostrare un linguaggio ausiliario.terence tao ha detto che sarebbe interessato a sapere se esistono altri esempi di progetti di crowdsourcing che esplorano gli spazi matematici e se ci sono lezioni apprese che possono essere utilizzate.tao zhexuan propone nuovi progetti
a tal fine, lo stesso tao ha proposto un progetto per testare ulteriormente questo paradigma.questo progetto è stato ispirato dalla domanda mathoverflow dell'anno scorso.subito dopo, tao zhexuan ne parlò ulteriormente sul suo mathstodon.questo problema appartiene al campo dell'algebra universale e comporta un'esplorazione su media scala della teoria delle equazioni semplici del gruppo originario (magma).il gruppo originale è un gruppo dotato di operazioni binariel'insieme g.inizialmente, a questa operazione o non sono associati assiomi aggiuntivi, quindi il gruppo originale stesso è una struttura relativamente semplice.naturalmente, aggiungendo ulteriori assiomi, come assiomi di identità o assiomi di associatività, possiamo ottenere oggetti matematici più familiari come gruppi, semigruppi o monoidi.qui siamo interessati agli assiomi (privi di costanti) di uguaglianza. questi assiomi riguardano l'uguaglianza delle espressioni costruite a partire dalle operazioni o e da una o più variabili sconosciute in g.due esempi familiari di tali assiomi sono la legge commutativa xoy = yox e la legge associativa (xoy) oz = xo (yoz).dove x, y, z sono variabili sconosciute nel gruppo originale g.d'altra parte, l'assioma di identità (a sinistra) eox = x non è qui considerato un assioma equazionale perché coinvolge una costante e ∈ g. tali assiomi che coinvolgono le costanti non vengono discussi in questo studio.successivamente, per illustrare il progetto di ricerca da lui avviato, terence tao ha introdotto undici esempi di assiomi di uguaglianza sui gruppi primitivi.questi assiomi di uguaglianza sono equazioni che coinvolgono solo operazioni di gruppo primitive e variabili sconosciute:quindi, ad esempio, l'equazione 7 rappresenta l'assioma commutativo, mentre l'equazione 10 rappresenta l'assioma associativo.l'assioma costante equazione 1 è il più forte, perché limita il gruppo originario g ad avere al massimo un elemento, al contrario, l'assioma riflessivo equazione 11 è il più debole, e tutti i gruppi originari soddisfano questo assioma;successivamente, possiamo esplorare la relazione di derivazione tra questi assiomi: quali assiomi possono dedurre quali assiomi?ad esempio, l'equazione 1 porta a tutti gli altri assiomi in questo elenco, che a loro volta portano all'equazione 11.l'equazione 8 può essere utilizzata come caso speciale per derivare l'equazione 9, che a sua volta può essere utilizzata come caso speciale per derivare l'equazione 10.la relazione di derivazione completa tra questi assiomi può essere descritta dal seguente diagramma di hasse:questo risultato risponde specificamente a una domanda sul sito web di domande e risposte sulla matematica mathoverflow: se esistono assiomi equazionali tra l'assioma costante (equazione 1) e l'assioma di associatività (equazione 10).vale la pena notare che la maggior parte delle relazioni di implicazione qui sono facili da dimostrare. esiste tuttavia una relazione di implicazione non banale.questa relazione è stata trovata in una risposta a un post di mathoverflow strettamente correlato alla domanda precedente:proposizione 1: l'equazione 4 implica l'equazione 7dimostrazione: supponiamo quindi che g soddisfi l'equazione 4in particolare, quando y = xox, ne consegue che (xox) o (xox) = (xox) ox.applicando nuovamente la (1), possiamo concludere che xox è idempotente:ora, sostituendo x con xox nella (1) e utilizzando la (2), otteniamo (xox) oy = yo (xox).in particolare, xox e yoy sono intercambiabili:inoltre, applicando la (1) due volte, otteniamo (xox) o (yoy) = (yoy) ox = xoy.pertanto, (3) può essere semplificato in xoy = yox, che è l'equazione 7.la formalizzazione del processo argomentativo di cui sopra può essere trovata in lean.vale la pena notare, tuttavia, che la questione generale di determinare se un insieme di assiomi di uguaglianza determina un altro insieme di assiomi di uguaglianza è indecidibile.pertanto, la situazione qui è in qualche modo simile alla sfida "busy beaver", cioè, dopo un certo punto di complessità, siamo destinati a incontrare problemi indecidibili ma prima di raggiungere questa soglia, speriamo ancora di scoprire problemi e fenomeni interessanti;il diagramma di hass sopra non solo asserisce le relazioni di implicazione tra gli assiomi di uguaglianza elencati, ma afferma anche le relazioni di non implicazione tra gli assiomi.ad esempio, come mostrato in figura, l'assioma commutativo dell'equazione 7 non implica l'assioma dell'equazione 4 (x + x) + y = y + x.per dimostrarlo, basta trovare un esempio di un gruppo primitivo che soddisfa l'assioma commutativo equazione 7 ma non soddisfa l'assioma equazione 4.ad esempio, in questo caso possiamo scegliere l'insieme di numeri naturali n, la cui operazione è xoy := x+y.più in generale, il diagramma afferma le seguenti relazioni di non implicazione, che (insieme alle relazioni di implicazione già notate) descrivono completamente l'insieme parzialmente ordinato di relazioni di implicazione tra questi undici assiomi:qui tao zhexuan invita i lettori a proporre controesempi per completare alcune dimostrazioni.il controesempio più difficile da trovare è che l’equazione 9 non può dedurre l’equazione 8.una soluzione può essere data utilizzando lean.inoltre, tao zhexuan fornisce anche un repository github che contiene prove lean di tutte le relazioni di inclusione e anti-inclusione di cui sopra.si può vedere che il solo calcolo del diagramma di haas di 11 equazioni è già un po’ complicato.il progetto proposto da terence tao è un tentativo di espandere questo diagramma di hass di diversi ordini di grandezza per coprire una gamma più ampia di insiemi di equazioni.l'insieme da lui proposto era ε, l'insieme di equazioni che utilizzava l'operazione di gruppo originale o al massimo quattro volte, finché gli assiomi di riflessività e simmetria delle equazioni sommarie non furono rietichettati.ciò include le undici equazioni menzionate sopra, ma ce ne sono molte altre.ricordiamo che il numero catalano c_n è il numero di modi per formare un'espressione utilizzando l'operazione binaria o (applicato a n+1 variabili segnaposto e data una stringa di m variabili segnaposto, il numero bell b_m è il numero di modi in cui sono queste variabili); nomi assegnati (che possono essere rietichettati), che consente di assegnare lo stesso nome a determinati segnaposto.pertanto, ignorando la simmetria, il numero di equazioni che coinvolgono al massimo quattro operazioni èil numero di equazioni i cui lati sinistro e destro sono uguali èquesti sono equivalenti agli assiomi riflessivi (equazione 11).le restanti 9118 equazioni appaiono in coppia a causa della simmetria delle equazioni, quindi la dimensione totale di ε è
tao zhexuan ha detto di non aver ancora generato un elenco completo di tali identità, ma sospetta che possa essere fatto facilmente utilizzando python.utilizzando gli strumenti di intelligenza artificiale, dovresti essere in grado di generare la maggior parte del codice richiesto.ha detto che non aveva idea di come sarebbe stata la geometria di ε.la maggior parte delle equazioni saranno incomparabili tra loro? sarà diviso in assiomi “forti” e assiomi “deboli”?ora, l'area messaggi di terence tao ha dozzine di commenti.lettori interessati, anche tao zhexuan ha esteso un invito a voi.
