Sanki süni intellekt hər həftə yeni bir riyaziyyat problemini həll edir. Ötən ay təkcə OpenAI sahənin ən çətin problemlərinin həllini iddia edən 719 əlyazmanı buraxdı. Hətta kompüter yoxlamaları da sürüşə bilər. İllərdir süni intellektin çöküşündən sonra, riyaziyyatın növbəti yeri olub olmadığını düşünmək düzgündür.
AxiomMath bahis edir ki, riyaziyyat bu taledən qaçmaq üçün yavaşlamır, daha sabit bir yerdə dayanır. 1.6 milyard dollarlıq startup süni intellekt agentlərinin proqram yazmaq və nəticədə elmi işləri aparmaq üçün etibar edə biləcəyi təsdiqlənmiş bir əsas qurmaq istəyir.
Çərşənbə günü şirkət, insanların yazdığı ən böyük riyaziyyat qurumlarından biri olan Stacks Layihəsini rəsmi olaraq təsdiqlədiyini elan etdi. Riyaziyyatçılar tez-tez Stacks-i nadir hallarda saxlayırlar. Kolumbiya riyaziyyatçısı Peter Woit layihəni məşhur Bourbaki kitabları ilə müqayisə edərək, 20-ci əsrdə riyaziyyatın əsasını yenidən qurmuş bir seriyaya bənzər heç nə olmadığını iddia edib.
Woits Columbia həmkarı Johan de Jong 2005-ci ildə Açıq mənbəli istinad kimi Stacks Layihəsini başladı. Riyazilar o vaxtdan bəri buna kömək ediblər, alicəbr, həndərə və say nəzəriyyəsi üzrə ən inkişaf etmiş fikirlərə qədər kollec səviyyəsində algəbrdən nəticələr qururlar.
Şirkətin süni intellekt agentləri flotu kitabxananın təxminən 7 654 səhifəsini təxminən 16 milyon satır kompüter tərəfindən yoxlanan kodla tərcümə edir.
Riyaziyyata formalaşmaq, onun altında olan qurumun sağlam olduğundan əmin olmaq üçün bir yoldur. Riyaziyyatçılar sübutunu Lean adlı proqramlaşdırma dilində kod kimi yenidən yazırlar və sübut köməkçisi adlı bir proqram kod xəttini bir xəttdən birinə yoxlayır. Əgər sübut keçirsə, riyaziyyatçılar bunun məntiqi olaraq etibarlı olduğuna güvənə bilərlər.
Xülasə — davamını mənbədə oxuyun.
