Maendeleo kumi katika hisabati na sayansi ya kompyuta ya kinadharia

Tunataka kuwawezesha wanasayansi na wanahisabati kwa zana zinazoharakisha uvumbuzi. Ndiyo maana hivi majuzi tulitangaza ChatGPT kwa Watafiti wa Kitaaluma⁠, mpango unaowapa wanasayansi na wanahisabati 100,000 ufikiaji bila malipo wa miundo yetu bora zaidi ya ChatGPT. Pia tunaendelea kutathmini miundo yetu kwa kutumia matatizo ya utafiti ambayo bado hayajatatuliwa wakati wa kuiunda.

Mwezi Mei, tulichapisha ukanushaji uliotolewa na AI⁠ wa dhana ya Erdős kuhusu umbali wa kipimo kimoja, uliogunduliwa tulipokuwa tukitathmini muundo ambao haujatolewa. Kazi hii tayari imechochea maendeleo zaidi katika hisabati na sayansi ya kompyuta ya kinadharia¹. Leo tunashiriki matokeo kumi yaliyochaguliwa, ambapo kila moja linatatua au kuleta maendeleo makubwa katika tatizo la muda mrefu ambalo halijatatuliwa. Matatizo haya yanahusu jiometri ya vipimo vingi, nadharia ya misimbo, uchangamano wa saketi za arithmetiki, nadharia ya makundi, aljebra za opereta, uchangamano wa kwanta, kriptografia ya latisi na kombinatoriki ya kikomo. Matatizo haya yote ni muhimu sana kwa jumuiya zao za kihisabati, na kadhaa yana umuhimu mpana katika hisabati kwa ujumla.

Tunatoa matokeo mapya kuhusu matatizo yafuatayo. Matokeo yalipatikana kwa kutumia toleo la ndani la Astra, muundo wetu mkuu unaofuata. Jumla ya tokeni zilizohitajika kupata suluhisho za matatizo haya ingegharimu takribani dola 2,000 kwa viwango vya Sol API. Kisha, wanadamu walitumia muundo huohuo kuandaa hoja hizi kuwa miswada. Baadaye, muundo ulirasimisha kila hoja katika cheti cha Lean⁠(fungua katika dirisha jipya). Pia tunatoa maelezo ya muundo kuhusu mchakato wake wa kufikiri kwa kila suluhisho.

1. Upangaji wa tufe katika vipimo vingi. Vikomo vipya vya juu vya msongamano wa upangaji wa tufe hadi kizingiti cha Cohn–Elkies.
2. Misimbo ya jozi na ya tufe: Vikomo vilivyoboreshwa kwa kiwango cha kipeo kuhusu ukubwa wa juu zaidi wa misimbo ya jozi katika umbali wowote wa chini uliowekwa, pamoja na matokeo yanayolingana kwa misimbo ya tufe yenye vipimo vingi.
3. Makundi yasiyo ya kisofiki. Uundaji unaothibitisha kuwepo kwa makundi yasiyo ya kisofiki, na hivyo kushughulikia swali kuu ambalo halijatatuliwa katika nadharia ya makundi.
4. Dhana ya uthabiti ya Connes. Ukanushaji wa dhana ya muda mrefu kwamba baadhi ya makundi huamuliwa kipekee na aljebra zake za von Neumann.
5. Uchangamano wa saketi za arithmetiki. Vikomo vipya vya chini vya kukokotoa permanenti kwa kutumia saketi na fomula za arithmetiki, ikiwemo kikomo cha chini cha fomula ya arithmetiki cha daraja la n⁴/log n.
6. Urudiaji sambamba wa kwanta. Nadharia ya urudiaji sambamba wa kipeo kwa michezo ya jumla ya kwanta ya wachezaji wawili, inayopanua kanuni ya msingi kutoka katika nadharia ya uchangamano wa kiklasiki.
7. Tatizo la vekta iliyo karibu zaidi. Ugumu wa ukadiriaji wa kipengele cha polinomu kwa tatizo la vekta iliyo karibu zaidi, swali la msingi la latisi linalohusiana na kriptografia ya baada ya kwanta.
8. Dhana ya ujazo ya Ehrhart. Kubainisha, katika kila kipimo, ujazo wa juu zaidi unaowezekana wa umbo konveksi ambalo kitovu chake ndicho nukta yake pekee ya ndani ya latisi.
9. Namba za Ramsey za rangi nyingi. Kikomo cha chini kinachozidi ukuaji wa kipeo kwa namba za Ramsey za pembetatu zenye rangi nyingi, kinachotatua tatizo la 183 la Erdős.
10. Dhana za namba za kikomo. Matokeo kuhusu dhana za ukompakti na udhoofu katika nadharia ya grafu za kikomo, yanayotatua matatizo ya 146 na 180 ya Erdős.

Kuibuka kwa mifumo inayoweza kuchangia utafiti wa hisabati kunazua maswali ambayo kampuni ya teknolojia haiwezi kuyajibu peke yake. Kuna mitazamo mingi kuhusu nafasi ya AI katika hisabati, na tunawaheshimu na kuwaelewa sana wale wanaohofia athari zake, wakiwemo waliotia saini Azimio la Leiden kuhusu AI na Hisabati⁠(fungua katika dirisha jipya). Tunaamini sifa zinazotolewa zinapaswa kuonyesha kwa uaminifu jinsi matokeo yalivyopatikana: kudai kwamba uthibitisho uliotolewa kikamilifu na mfumo wa AI ni kazi ya wanadamu kungewasilisha vibaya mchango wa mfumo na asili ya kazi halisi ya kiakili ya wanadamu. Tulisaidia kuandaa miswada na kurasimisha uthibitisho katika Lean, na tunawajibikia usahihi wake, ingawa hoja zenyewe za kihisabati zilitolewa na mfumo wetu. Tunatumaini jumuiya ya wanahisabati itachunguza matokeo haya kwa kina, itayaweka katika muktadha na kuyahuisha mawazo yaliyo nyuma yake kupitia utafiti na uvumbuzi mpya.

Mifumo ya AI inapokuwa washirika wa utafiti wenye uwezo wa juu zaidi, kuhakikisha ufikiaji mpana ni muhimu ili kuwawezesha wanasayansi na wanahisabati kuamua na kuelekeza mustakabali wa taaluma zao katika enzi hii ya mabadiliko makubwa.