di
Sergio Donato
Il caso OpenAI ha attirato l’attenzione, ma AlphaProof Nexus ha chiuso 9 problemi di Erdős con verifiche formali in Lean. Il contributo dell’IA nella matematica è comunque ormai palpabile
La scorsa settimana, OpenAI ha annunciato che un suo modello interno ha confutato una congettura di geometria discreta rimasta aperta per quasi 80 anni. Il problema (il numero 90) era stato posto da Paul Erdős nel 1946 e parte da una domanda facile da visualizzare: se si dispongono n punti su un piano, quante coppie possono trovarsi esattamente alla distanza di 1?
Per decenni la risposta più credibile è stata legata alla griglia. Erdős aveva costruito esempi molto efficienti e aveva congetturato che, andando verso numeri di punti sempre più grandi, nessuna rappresentazione che fosse una griglia potesse fare molto meglio. In forma tecnica, il limite atteso era n^(1+o(1)): una crescita appena superiore a quella lineare, con un vantaggio nell’esponente destinato a ridursi.Finora il metodo migliore per avvicinarsi alla congettura di Erdős usava una griglia quadrata ridimensionata, capace di generare molte coppie di punti separate dalla stessa distanza
