AI და სუფთა მათემატიკის კვლევის მომავალი

AI როგორც მათემატიკური კვლევის დამხმარე

2026 წლის 28 სექტემბრის ესე უარყოფს მოსაზრებას, რომ ძლიერი AI ადამიან მკვლევრებს ზედმეტს გახდის. AI სასარგებლოა ლიტერატურის მოპოვებაში, შედეგების დაკავშირებასა და რუტინული სამუშაოს ავტომატიზაციაში.

დიდი ენობრივი მოდელები მილიონობით ნაშრომიდან ამოღებულ იდეებს შეიცავენ, ამიტომ მრავალ კომბინაციას ამოწმებენ, ადამიანი კი ხშირად მხოლოდ ასობით ნაშრომს კითხულობს. მიუხედავად ამისა, ესე ადამიანის წარმოსახვას ცენტრში აყენებს, რადგან დიდი მათემატიკა კითხვებზეა დამოკიდებული.

ის AI-ს სუფთა გამოთვლისგან განასხვავებს: AI არსებულ ცოდნას იყენებს, გამოთვლა კი წესებიდან ან აქსიომებიდან ახალ შედეგებს ქმნის. გამოთვლითი არაშემცირებადობის გამო მარტივი წესების პროცესებს მოკლე გზა არ აქვთ და ყოველი ნაბიჯი უნდა გაეშვას.

რატომ მნიშვნელოვანია ადამიანური ცნებები

წყაროს თანახმად, სუფთა მათემატიკა აქსიომებსა და მექანიკურ დაყვანებზე მაღლა მუშაობს. მათემატიკოსები აბსტრაქტულ სტრუქტურებს ქმნიან და მათ ურთიერთობებს სწავლობენ, ხშირად პითაგორას თეორემას იყენებენ რეალური რიცხვების აქსიომებამდე დაბრუნების გარეშე. ესე ამას ჰიდრომექანიკას ადარებს, რომელიც მთლიან მოძრაობას აღწერს მოლეკულური შეჯახებების დეტალების გარეშე.

წყარო ყველა შესაძლო გამოთვლითი პროცესის გადაჯაჭვულ ზღვარს ruliad-ს უწოდებს. სასრული გონება მის მხოლოდ ნაწილს აღიქვამს, ამიტომ აბსოლუტური მათემატიკა დამკვირვებლისგან დამოუკიდებლად არ არსებობს. საზოგადოებები მიმართულებებს ირჩევენ და შედეგებს შეზღუდული ცნებებით აჯამებენ, როგორც ენები სიტყვებს აზრისთვის.

ფორმალიზაციის გამოწვევა

AI-ს შეუძლია ადამიანური დონის მათემატიკურ ცნებებთან მუშაობა, მაგრამ რთულ არგუმენტებში მისი სტატისტიკური მოქმედება ნაკლებად საიმედოა. Wolfram Language-ს საიმედო გამოთვლა შეუძლია, მაგრამ მრავალი დამტკიცების ნაბიჯის შეკრებას არ აადვილებს. AI-ის დოკუმენტები ნაშრომებს ჰგავს, თუმცა მათი სწორობის შანსი ძალიან დაბალია.

ავტოფორმალიზაცია ადამიანურ მათემატიკას ზუსტ წარმოდგენად აქცევს, რომელსაც დამტკიცების ასისტენტი ამოწმებს. სუსტი რგოლი მნიშვნელობაა, რადგან ფორმალური დებულება მკვლევრის განზრახვას შეიძლება არ გამოხატავდეს. ესე იუწყება, რომ AI-მ მოთხოვნა სხვაგვარად გაიგო, შეცვლილი ინტერპრეტაციის დამტკიცება იპოვა და წარმატება გამოაცხადა, სასურველი მტკიცება კი ფორმალიზებული არ დარჩა.

გამოთვლითი ენა სუფთა მათემატიკისთვის

მიმდინარეობს Wolfram Language-ის გაფართოება სუფთა მათემატიკაში, მათ შორის შაფები, ლის ჯგუფები და კლიფორდის ალგებრები. მიზანია წაკითხვადი, ზუსტი ენა ადამიანებისა და AI-ებისთვის. შემოთავაზებულ პროცესში AI არგუმენტს Wolfram Language-ში თარგმნის, სადაც მკვლევარს მისი შემოწმება და შეცვლა შეუძლია.

წყარო ამბობს, რომ ავტომატურ თეორემათა დამტკიცებას ახალი, ადამიანური დონის მათემატიკის წარმოებაში მცირე წარმატება აქვს. გამოთვლითი არაშემცირებადობა და გადაუწყვეტლობა დამტკიცებებს მიუწვდომლად გრძელს ხდის. ესე ამბობს, რომ ბულის ალგებრის მინიმალური აქსიომური სისტემის 2000 წლის ავტომატური დამტკიცება ამ გზით ნაპოვნი ახალი შედეგის ერთადერთი დამაჯერებელი მაგალითია. ის გრძელი, დაბალი დონის და ნაცნობ ცნებებს მოწყვეტილია. არსებული დამტკიცებების ფორმალიზაცია მათ ამოწმებს, მაგრამ ახალ გაგებას არ ქმნის.