Axiom: ИИ-агеннар үөрдэрэ 24 хонукка математика саамай уһун дакаастабылын — муҥур боростуой бөлөхтөр классификацияларын — машинанан бэрэбиэркэлээтилэр
Стартап «улахан теорема» Lean-ҥа 43,1 мөл. устуруокалаах формализациятын таһаарда уонна бэчээттэммит литератураттан 34 улахан туораһыны булбутун эттэ. Атын бөлөхтөр өссө туспа хос оҥорбот буолбуттар.
ИИ-стартап Axiom муҥур боростуой бөлөхтөр классификацияларын (CFSG) бастакы толору компьютерынан бэрэбиэркэлэммит дакаастабылын оҥорбутун этэр — бу муҥур симметрия «атомнарын» барытын ааҕар түмүк. Дьон суруйбут бастакы дакаастабыла 100-ҕэ чугас математик 500-тэн элбэх ыстатыйатыгар 15 000-ҥа чугас сирэйи ылар.
Хайдах оҥоһуллубутай
Axiom алтынньы 26 күнүнээҕи отчуотунан, инженердэр уонна математиктар 24 хонук (2026 сыл алтынньы 1–2 күнүттэн) хас да уон ИИ-агеннардаах үөрдэри салайан, Lean дакаастабыл систематыгар 43,1 мөл. кэриҥэ устуруока куоду оҥорбуттар; Lean хас биир логическай хардыыны бэрэбиэркэлиир. Үлэ «бастакы көлүөнэ» дакаастабылынан барбыт, Mathlib-ка олоҕурбут, 108 түһүмэххэ уонна 380-ча сорукка араарыллыбыт. Агеннар, атын да түмүктэр иһигэр, Монстр бөлөх боростуойун дакаастаабыттар.
Машиналар тугу булбуттарай
Литератураҕа булуллубут боппуруостар үксүлэрэ кыра этилэр (сыыһа суруйуулар, табылыысса алҕастара, тохтоппут усулуобуйалар), ол эрээри Axiom бэчээттэммиттэн 34 улахан туораһыны этэр. Саамай улахана тэҥнэспэт бөлөхтөр теоремаларыгар сыһыаннаах: агеннар Джон Уолтер 1986 сыллааҕы толкуйун биир хардыытыгар контрпримердары булбуттар, онтон хамаанда атын суолу тутан таһаарбыт, ол иһигэр системата дакаастаабыт саҥа түмүгү — бөлөх теоретиктара Ричард Лайонс уонна Рональд Соломон сүбэлэрин кэнниттэн. Axiom алҕастар испииһэктэрин таһаарарга эрэннэрэр.
Сэрэтии
Lean түмүктээһиннэри бэрэбиэркэлиир, ол эрээри формальнай этиилэр уонна быһаарыылар наадалаах теораманы чахчы көрдөрөллөрүн дьон бигэргэтиэхтээхтэр. Алтынньы 27 күнүнээҕи СМИ иһитиннэриилэринэн, ханнык да таһыттан бөлөх дакаастабылы толору туспа хос оҥоро илик; Axiom оннук кыах буоларын туһугар репозиторийын уонна сборка артефактарын таһаарбыт. Этиилэр компания бэйэтин отчуотунан.