Avviso: avevo dato accesso anticipato alla versione beta interna di Grok 4.20 Ha trovato una nuova funzione di Bellman per uno dei problemi su cui stavo lavorando con il mio studente N. Alpay. Il problema si riduce all'identificazione della funzione massimale punto per punto U(p,q) sotto due vincoli e alla comprensione del comportamento di U(p,0). Nel nostro articolo abbiamo dimostrato che U(p,0)\geq I(p), dove I(p) è il profilo isoperimetrico gaussiano, I(p) ~ p\sqrt{log(1/p)} quando p ~ 0. Dopo ~5 minuti, Grok 4.20 ha prodotto una formula esplicita U(p,q) = E \sqrt{q^2+\tau}, dove \tau è il tempo di uscita del moto browniano da (0,1) partendo da p. Questo porta a U(p,0)=E\sqrt{\tau} ~ p log(1/p) quando p ~ 0, un miglioramento della radice quadrata nel fattore logaritmico. Qual è il significato di questo risultato? Non ti dirà come cambiare il mondo domani. Piuttosto, fornisce un piccolo passo verso la comprensione di cosa sta succedendo con le medie degli analoghi stocastici delle derivate (variazione quadratica) delle funzioni booleane: quanto possono essere piccole? Più precisamente, questo fornisce un limite inferiore netto sulla norma L1 della funzione quadratica diadiaca applicata alle funzioni indicatrici 1_A degli insiemi A \subset [0,1]. Nel mio precedente tweet sulla funzione di Takagi, abbiamo visto che il limite inferiore netto su ||S_1(1_A)||_1 coincide miracoloso con la funzione di Takagi di |A| che (sorprendentemente per me) è correlata all'ipotesi di Riemann. Qui, otteniamo un limite inferiore netto su ||S_2(1_A)||_1 dato da E \sqrt{\tau}, dove il moto browniano inizia da |A|. Questa funzione appartiene alla famiglia dei profili di tipo isoperimetrico, ma a differenza della funzione frattale di Takagi, è liscia e non coincide con il profilo isoperimetrico gaussiano. Infine, nell'analisi armonica è noto che la funzione quadratica non è limitata in L^1. La domanda qui era più per curiosità: come esattamente esplode quando testata su funzioni booleane 1_A. In precedenza, il miglior limite inferiore noto era |A|(1-|A|) (Burkholder—Davis—Gandy). Nel nostro articolo, abbiamo ottenuto |A| (1-|A|)\sqrt{log(1/(|A|(1-|A|)))}. Questa nuova funzione di Bellman di Grok dà |A| (1-|A|) \log(1/(|A|(1-|A|))) e questo limite è effettivamente netto.

Se continui a testare i problemi di Erdős con i LLM, è molto probabile che alla fine risolverai uno di quelli aperti. Gli esperti non lo stanno facendo (per ovvi motivi). I non esperti presumono che gli esperti lo stiano facendo. Non lo stanno facendo.

Installa Aristotle. Ottieni la chiave API. Eseguilo dal tuo terminale. Scegli un problema aperto in matematica e inseriscilo in aristotle (nella sua lingua naturale!). Dopo diverse ore, produrrà una prova formale completa in lean oppure potrebbe fallire. 👏