Ongelooflijk, deze naamGauss(Gauss)’s nieuwe AI-agent voelt een beetje gek. Omdat het alleen maar gebruiktdrie wekentijd, het is klaarTerence Taoen de wiskundige uitdaging van Alex Kontorovich om de Priemgetalstelling (PNT) in Lean te formaliseren.


Weet je, nadat Tao Zhexuan en Kontorovich deze uitdaging in januari 2024 hadden voorgesteld, brachten ze veel tijd door18 maanden(juli dit jaar) is er slechts gefaseerde vooruitgang geboekt.

Dus wat is de oorsprong van deze Gauss?

Daarachter staat een bedrijf genaamdWiskundeVolgens rapporten is Gauss de eerste die topwiskundigen assisteert bij formele verificatieautomatische formalisering(autoformalisatie)Agent:


Formalisering verwijst hier naar het omzetten van door mensen geschreven wiskundige inhoud in een machinaal leesbare, controleerbare, strikte en ondubbelzinnige formele taal, en vervolgens het gebruik van computers om de juistheid ervan te helpen verifiëren.

De reden waarom Tao Zhexuan en Alex Kontorovich tot nu toe slechts gefaseerde vooruitgang hebben geboekt, is dat het probleem blijft hangen bij het kernprobleem van complexe analyse.

Als leven op basis van silicium wordt deze Gauss gekenmerkt door zijn vermogen om non-stop te werken, wat de werklast aanzienlijk vermindert die alleen formele topexperts in het verleden konden voltooien; Tegelijkertijd formaliseerde Gauss ook de belangrijkste ontbrekende resultaten in de hierboven genoemde complexe analyse.

Dit is de reden waarom het de wiskunde-uitdaging die Terence Tao in 18 maanden niet voltooide, in drie weken kan oplossen.

Hoe wordt Gauss geïmplementeerd?

Momenteel heeft Math Company nog geen officieel technisch rapport uitgebracht.

Maar afgaande op het eindresultaat genereerde Gauss ongeveer 25.000 regels Lean-code, met daarin duizenden stellingen en definities.

Het duurde vaak jaren voordat formele bewijzen van deze omvang klaar waren.

De grootste formele projecten in de geschiedenis (die vaak zelfs tien jaar bestrijken) zijn slechts een orde van grootte groter dan dit (tot 500.000 regels code).

Ter vergelijking: de standaard wiskundebibliotheek Mathlib van Lean heeft ongeveer 2 miljoen regels code en 350.000 stellingen, maar het kostte meer dan 600 bijdragers acht jaar om te bouwen.


Om de werking van Gauss te ondersteunen, werkte het team ook samen met Morph Labs om de Trinity-omgevingsinfrastructuur te ontwikkelen.

Omdat het uitvoeren van Gauss op zo'n grote schaal duizenden gelijktijdige agenten nodig zal hebben, en elke agent zijn eigen Lean-besturingsomgeving heeft, die verschillende terabytes aan clustergeheugen zal verbruiken, waardoor het een uiterst complexe uitdaging op het gebied van systeemtechniek wordt.

Het Math-team verklaarde ook:

Gauss zal de tijd die nodig is om grote wiskundeprojecten te voltooien aanzienlijk verkorten.

Naarmate algoritmen blijven verbeteren, zijn we van plan de totale hoeveelheid formele code in de komende twaalf maanden met honderd tot duizend keer te vergroten.

Dit zal het oefenterrein zijn voor nieuwe paradigma’s – richting ‘verifieerbare superintelligentie’ en ‘generalistische machinewiskundigen’.

En zojuist,Terence TaoIk heb enkele kwesties uitgelegd die verband houden met de formalisering van Mastodon (het volgende is de verklaring van Tao Zhexuan).

Projecten van welke complexiteit dan ook hebben doorgaans expliciet gestelde doelen en impliciete, niet-uitgesproken doelen. Het gestelde doel van een Lean-formalisatieproject zou bijvoorbeeld kunnen zijn om een ​​formeel bewijs te verkrijgen van een of andere wiskundige stelling …; leer hoe u verschillende samenwerkingshulpmiddelen kunt gebruiken en taken kunt toewijzen; ontdek op organische wijze de fijnere structuur van bewijzen van

In het verleden was het vaak niet nodig om deze impliciete doelen te formuleren, omdat er een sterke empirische correlatie bestond tussen het bereiken van deze doelen en het bereiken van expliciete doelen. In het geval van formele projecten zal vrijwel elke mensgerichte poging om expliciete doelen te bereiken uiteindelijk en op natuurlijke wijze de meeste van de hierboven genoemde impliciete doelen bereiken. Zo worden expliciete doelen effectief een haalbaar alternatief voor bredere praktische doelen.

De zaken veranderen echter met de opkomst van krachtige AI-tools die een heel andere aanpak hanteren dan mensen. Deze hulpmiddelen kunnen worden ingezet om een ​​expliciet doel op te lossen zonder alle impliciete doelen te hoeven bereiken die tegelijkertijd zouden kunnen worden bereikt als de taak door een menselijk team zou worden uitgevoerd. In feite dicteert de aard van AI-optimalisatiealgoritmen dat ze zelfs hoge prestaties op expliciete doelen kunnen bereiken, ten koste van alle impliciete doelen. (Zie de wet van Goodhart: "Wanneer een maatregel een doel wordt, is deze niet langer een goede maatregel.")

Gezien de toenemende inzet van deze instrumenten, duidt dit erop dat projectorganisatoren nu een grotere inspanning moeten leveren om alle doelstellingen van een project duidelijk te formuleren, en niet alleen de nominale doelstellingen. In sommige gevallen zijn deze doelen misschien niet eens in eerste instantie duidelijk voor de organisatoren zelf en vereisen ze enige discussie tussen de deelnemers. Externe partijen die geïnteresseerd zijn in het testen van dergelijke projecten met hun AI-tools moeten vooraf met de organisatoren overleggen voor het geval ze een of meer belangrijke impliciete doelen missen die hun tools niet zullen optimaliseren.


De oprichter is de auteur van de ICML’25 Time Test Award

Het is vermeldenswaard dat de baas van het Math-bedrijf ook enige kracht heeft.

Omdat hij een van de auteurs is van het artikel dat dit jaar op de AI-conferentie de ICML Time Test Award won.Christian Szegedy.


Dit artikel is Batch Normalization (Batch Normalization, ook wel BatchNorm genoemd), voorgesteld door hem en een andere auteur Sergey Loffe in 2015.


Tegenwoordig is dit artikel meer dan 60.000 keer geciteerd. Het is een mijlpaal doorbraak in de geschiedenis van de ontwikkeling van deep learning en heeft de training en toepassing van diepe neurale netwerken enorm bevorderd.

Er kan worden gezegd dat het een van de sleuteltechnologieën is die het mogelijk maakt dat diepgaand leren zich kan ontwikkelen van kleinschalige experimenten naar grootschalige bruikbaarheid en betrouwbaarheid.

Hoewel netizens Amazing uitriepen na het lezen van Gauss, riepen ze de functionaris natuurlijk ook op om de krant snel vrij te geven.

Wat de meer gedetailleerde technische inhoud betreft, kunnen we een kijkje nemen~