Disclaimer: Ik had vroege toegang gegeven tot de interne bètaversie van Grok 4.20 Het vond een nieuwe Bellman-functie voor een van de problemen waar ik aan werkte met mijn student N. Alpay. Het probleem reduceert tot het identificeren van de puntgewijze maximale functie U(p,q) onder twee beperkingen en het begrijpen van het gedrag van U(p,0). In ons paper hebben we bewezen dat U(p,0)\geq I(p), waarbij I(p) het Gaussische isoperimetrische profiel is, I(p) ~ p\sqrt{log(1/p)} als p ~ 0. Na ~5 minuten produceerde Grok 4.20 een expliciete formule U(p,q) = E \sqrt{q^2+\tau}, waarbij \tau de tijd is dat de Browniaanse beweging het interval (0,1) verlaat, beginnend bij p. Dit levert U(p,0)=E\sqrt{\tau} ~ p log(1/p) op bij p ~ 0, een vierkantswortelverbetering in de logaritmische factor. Heeft dit resultaat enige betekenis? Het zal je niet vertellen hoe je de wereld morgen kunt veranderen. Het geeft eerder een kleine stap richting het begrijpen van wat er aan de hand is met gemiddelden van stochastische analogen van afgeleiden (kwadratische variatie) van Booleaanse functies: hoe klein kunnen ze zijn? Meer precies, dit geeft een scherpe ondergrens voor de L1-norm van de dyadische vierkante functie toegepast op indicatorfuncties 1_A van verzamelingen A \subset [0,1]. In mijn vorige tweet over de Takagi-functie zagen we dat de scherpe ondergrens op ||S_1(1_A)||_1 miraculously samenvalt met de Takagi-functie van |A| die (verrassend voor mij) gerelateerd is aan de Riemann-hypothese. Hier verkrijgen we een scherpe ondergrens op ||S_2(1_A)||_1 gegeven door E \sqrt{\tau}, waarbij de Browniaanse beweging begint bij |A|. Deze functie behoort tot de familie van isoperimetrische-type profielen, maar in tegenstelling tot de fractale Takagi-functie, is het glad en komt het niet overeen met het Gaussische isoperimetrische profiel. Ten slotte is het in de harmonische analyse bekend dat de vierkante functie niet gebonden is in L^1. De vraag hier was meer uit nieuwsgierigheid: hoe precies explodeert het wanneer het getest wordt op Booleaanse functies 1_A. Eerder was de beste bekende ondergrens |A|(1-|A|) (Burkholder—Davis—Gandy). In ons paper hebben we |A| (1-|A|)\sqrt{log(1/(|A|(1-|A|)))} verkregen. Deze nieuwe Bellman-functie van Grok geeft |A| (1-|A|) \log(1/(|A|(1-|A|))) en deze ondergrens is eigenlijk scherp.

Als je blijft testen met Erdős-problemen met LLM's, is de kans groot dat je uiteindelijk een van de openstaande problemen oplost. Experts doen dit niet (om voor de hand liggende redenen). Niet-experts gaan ervan uit dat de experts het doen. Dat doen ze niet.

Installeer Aristotle. Verkrijg een API-sleutel. Voer het uit vanuit je terminal. Kies een open probleem in de wiskunde en voer het in Aristotle in (in zijn natuurlijke taal!). Na enkele uren zal het ofwel een volledige formele Lean-bewijs produceren of het kan falen. 👏