Lean-ის თეორემების დამმტკიცებელი სანდოობის კითხვების წინაშე დგას, რადგან AI-ის ავტოფორმალიზაცია ვითარდება

ფორმალიზაცია და ავტოფორმალიზაცია

Lean-ი მათემატიკოსებში ყველაზე პოპულარული თეორემების დამმტკიცებელი გახდა, მათემატიკოს თომას ჰეილსის სტუმრის პოსტის მიხედვით. ის ლეო დე მოურამ 2013 წელს Microsoft-ში მუშაობისას შექმნა; Microsoft-მა მოგვიანებით პროგრამა ღია კოდით გამოაქვეყნა. Lean-ი ტიპების თეორიაზეა დაფუძნებული, კერძოდ, ინდუქციური კონსტრუქციების კალკულუსის დიალექტზე. მისი საზოგადოებრივი ბიბლიოთეკა mathlib, რომელიც 2017 წელს დაიწყო, ახლა დაახლოებით 300 000 თეორემას, 100 000-ზე მეტ განსაზღვრებას, 2,5 მილიონი კოდის ხაზს და 700-ზე მეტ კონტრიბუტორს მოიცავს. mathlib-ის ნებისმიერი თეორემა შეიძლება მომდევნო დამტკიცებებში მოჰყავდეს ხელახლა დამტკიცების ნაცვლად.

ავტოფორმალიზაცია, როცა AI კითხულობს ნაშრომს და გამოსცემს ფორმალურ დამტკიცებას, 2026 წელს პრაქტიკულ რეალობად იქცა. მნიშვნელოვან ეტაპებს შორისაა: მარტივი რიცხვების თეორემის კვაზი-ავტოფორმალიზაცია Math Inc.-ის მიერ 2025 წლის სექტემბერში, Munkres-ის ტოპოლოგიის სახელმძღვანელოს დიდი ნაწილის ფორმალიზაცია, სფეროთა შეფუთვის ამოცანა 24 განზომილებაში, Anthropic-ის მიერ ფერმას უკანასკნელი თეორემის ავტოფორმალიზაცია 4 სექტემბერს, რომელმაც 11 დღეში 13 მილიონი ხაზი Lean დააგენერირა, და OpenAI-ს Navier-Stokes-ის აფეთქების ფორმალიზაცია, რომელიც 8 სექტემბერს გამოცხადდა.

დიზაინი და სანდოობის მოდელი

Lean-ი აერთიანებს ზოგადი დანიშნულების პროგრამირების ენას მათემატიკურ ენასთან განსაზღვრებებისთვის, თეორემების ფორმულირებებისთვის და დამტკიცების სკრიპტებისთვის. დამტკიცების სკრიპტებს პარსავს, ამუშავებს და ამოწმებს Lean-ის ბირთვი, C++ კოდის რამდენიმე ათასი ხაზი. პოსტში ხაზგასმულია, რომ Lean-ის დამტკიცებები არასოდეს უნდა იწამოს ბირთვის მიერ შემოწმებამდე და რომ საჭიროა ცალკე ადამიანური აუდიტი ფორმულირების ერთგულების დასადასტურებლად, რომ დადასტურებული თეორემა ნამდვილად ის თეორემაა, რომელიც მათემატიკოსებს გულისხმიათ.

სანდოობის ხარვეზების ზაფხული

სანდოობის ხარვეზი არის ბირთვის ხარვეზი, რომელიც უშვებს „False“-ის დამტკიცებას და, შესაბამისად, ნებისმიერი წინადადების დამტკიცებას. რამდენიმე ასეთი ხარვეზი Lean-ში 2026 წლის ივლისსა და აგვისტოში გამოვლინდა, რასაც ახლა სანდოობის ხარვეზების ზაფხულს უწოდებენ. ერთმა ხარვეზმა კოლატცის ჰიპოთეზის უკანონო უარყოფა გამოიწვია, მეორემ კი კეპლერის ჰიპოთეზის მოკლე უკანონო დამტკიცება. ყველა მათგანი სწრაფად გამოსწორდა და mathlib-ი გამოსწორებული ბირთვით შემოწმდა.

წინადადებები და ღია პრობლემები

განიხილება სამი პასუხი. პირველი, დაწერეთ დამატებითი Lean-ის ბირთვები და ჯვარედინად შეამოწმეთ დამტკიცებები; დაახლოებით 25 ბირთვი არსებობს და Navier-Stokes-ის ფორმალიზაცია ათზე მეტმა დამტკიცების შემმოწმებელმა დაადასტურა. მეორე, ფორმალურად გადაამოწმეთ ბირთვი, როგორც იოახიმ ბრაიტნერმა გააკეთა Con-Leche-ით, დადასტურებული Lean-ის ბირთვით, რომლის თანმიმდევრულობის დამტკიცება Claude-ით დაგენერირდა და რომელმაც mathlib შეამოწმა. მესამე, გაიღრმავეთ Lean-ის ტიპების თეორიის თეორიული გაგება, სადაც უნიკალური ტიპიზაცია, Pi-ინექტიურობა, შეცვლილი Church-Rosser-ის თვისება და სრული საჯარო ფარდობითი თანმიმდევრულობის დამტკიცება ჯერ კიდევ ღიაა. პოსტი სრულდება კენ ტომპსონის „Reflections on Trusting Trust“-ის ციტირებით და აფრთხილებს, რომ ბრმა ნდობა ისეთი სისტემების მიმართ, როგორიც Lean-ია, აღარ არის შესაძლებელი.

წყაროები: terrytao.wordpress.com