Theorem.chat տարեկան
Theorem.chat-ը վերցնում է մաթեմատիկական պնդում և փորձում է լուծել այն։ Դուք նշում եք պնդումը և ստանդարտները, որոնց այն պետք է համապատասխանի։ ԱԻ մոդելների մի խումբ՝ այնքան, որքան ցանկանում եք, ցանկացած արտադրողից՝ հարձակվում է դրա վրա, և մեկ այլ մոդել դատավոր է։ Այնուհետև արկածը ֆորմալացվում է Lean 4-ում Mathlib-ի դեմ, և Lean kernel-ը որոշում է, թե արդյոք այն ապացուցված է։ Այս վերջին քայլն է արտադրանքը։
Ինչու՞ kernel, և ոչ այլ մոդել
Հարցրեք մոդելի դժվար հարց և դուք կստանաք ճիշտ պատասխան, թե ոչ։ Հարցրեք մի քանիսին և նրանք հաճախ համաձայնվում են, ինչը համոզիչ է, բայց ոչ այնքան։ Մասնավորապես, մոդելները կիսվում են ուսուցման տվյալներով և կիսվում են կույր կետեր։ Երկրորդ մոդելը՝ առաջինը ստուգելու համար, նույնպես նույն տեսակի դատողություն է, և այն կարող է քննարկվել։ Lean kernel- ը չի կարող։ Այն կամ ելնում է ակսիոմներից և Mathlib- ից, կամ էլ ոչ, և վստահությունը չի ազդում արդյունքի վրա։
Պարզապես ստուգվում են և մերժվում են օրինական ապացույցը կեղծելու սովորական ձևերը։ Պարզաբանումը, որը թողնում է sorry-ի հետ խողովակ, որը դիմում է native_decide-ին՝ ստիպելով kernel-ին անել հաշվարկներ վստահության վրա, կամ այն, որը անձայն ներմուծում է նոր ակսիոմ, հայտնաբերվում է և մերժվում է, այլ ոչ թե հաշվվում որպես հաջողություն։
Ի՞նչ կարող է անել վահանակը
Պատճառաբանությունը ամենաէժան մասն է։ Պլանշետը աշխատում է գրականության հետ՝ arXiv, OpenAlex, Crossref, այնպես որ հայտնի արդյունքը հղվում է, այլ ոչ թե վատ վերարտադրվում։ Այն ունի SageMath և PARI/GP հաշվարկների համար, Z3 և CVC5 SMT լուծման համար, OEIS որոնում իր կողմից կառուցված հաջորդականության հայտնաբերման համար և Python- ի sandbox- ի միջավայր ցանցի մուտք չունենալով։ Հնարավոր է թեզը փորձարկել 10 հազար դեպքերի դեմ, մինչև որևէ մեկը փորձի ապացուցել այն, և հակաօրինակը անմիջապես ավարտում է քննարկումը։
Պատճառներ, ոչ թե լեզուներ
Համապատասխանությունը չի գնահատվում արկածների որակի վրա։ Պատճառը բաժանվում է ընդունման կանոնների վրա, և կանոնը միայն այն ժամանակ է որոշվում, երբ դրա հետևում գտնվող ինչ- որ բան կարող է վերահսկվել երրորդ կողմի կողմից՝ աղբյուրի հետ կապված հատվածի մեջբերմամբ, կամ կոդ, որը իրականում իրականացվել է իր իրական արտադրանքի հետ։ Դատավորը վերահսկում է այդ ապացույցը մինչև որոշում կայացնելը, և չի կարող հայտարարել համապատասխանությունը ավարտված, քանի դեռ կանոնը բաց է։
Դու ես սահմանել աստիճանը
Ստանդարտը ձեր ընտրության հարցն է, և դատավորը գրեթե անմիջապես ընդունում է այն։ Պարզապես հարցրեք, թե ինչ է ընդունում ուշադիր մասնագետ, և դուք կստանաք այն։ Պարզապես հարցրեք, թե ինչ է ասում ամբողջական սկզբունքը՝ յուրաքանչյուր ենթադրության հետ, և դուք կստանաք դատավճիռը։ Պարզապես հարցրեք, թե ինչ աստիճանի արժանի է մրցանակը, և ազնիվ արդյունքը հաճախ ճշգրիտ հաշվարկ է, թե որտեղ է խումբը սխալվել, որը ավելի շատ արժե, քան վստահելի պնդումը, որը դուք պետք է ինքներդ ստուգեք։
Պարզ ասած՝ սա այնպիսի մեքենա չէ, որը լուծում է բաց խնդիրներ։ Սա այնպիսի մեքենա է, որը չի ընդունում արկածախնդրությունը որպես լուծված, երբ այն այդպես չէ, և որը ճիշտ է ասում, թե որ քայլը ձախողվել է։
Անհաջողված ֆորմալացումը օգտակար ելք է
Երբ Lean- ը չի փակում ապացույցը, դուք ստանում եք ճիշտ նպատակը, որը մնացել է։ Պրակտիկայում դա հաճախ այն վայրն է, որտեղ անօթևան վիճաբանությունը ձեռքի շարժում էր՝ քայլ, որը բոլորը կարդացել են բանաստեղծական տարբերակը։ Այնուհետև այդ նպատակը փոխանցվում է այն տեղին, որը լավագույն տեղն է դրանք հարձակվելու համար, միասին այն ամենի հետ, ինչ արդեն փորձվել է, և ոչինչ այլ։ Մոլեկուլները ջախջախվում են, երբ նրանք կախված են, կրկնում են իրենց ամբողջ արժեքը, փոխարենը մեկ հատուկ հարցը հաճախ բացում է տոկոսների մի մասը։
Չորս տարի շարունակ աշխատելուց հետո նա փրկվեց։
Յուրաքանչյուր լեմմա, որը ցուցակը հաստատում է, իր ապացույցով մտնում է կիսաշրջանառության գրադարան, այնպես որ արդյունքները գրվում են մեկ անգամ և երբեք չեն վերադառնում, իսկ կիսատ թողնվածները գրանցվում են, որպեսզի ոչ ոք չվերադառնա։ Համապատասխանությունները աշխատում են սերվերի կողմից և կանգ են առնում՝ բյուջեի, մատուցողի անջատման կամ էջը փակելու պատճառով, և շարունակվում են հենց այնտեղ, որտեղ դադարել են։
Ինչի՞ համար չէ
Թեորեմը եզրակացական բառ է։ Այս կայքը ստեղծվել է մաթեմատիկայի, տրամաբանության, տեսական համակարգչային գիտության, տեսական ֆիզիկայի և տնտեսական տեսության համար՝ այնպիսի ոլորտներ, որտեղ պնդումը հաստատվում է ապացույցով։ Բիոլոգիայի, բժշկության, քիմիայի կամ հասարակական գիտությունների փորձնական հարցերը չեն առաջացնում թեորեմներ, այլ դրանք առաջացնում են հայտնաբերումներ, և ոչ մի ֆորմալացում չի կարող որոշել դրանք։ Մեր քույր կայքը referee.chat- ը նույնպես գործում է նույն panel- and- referee գործընթացը առանց Lean քայլերի, հենց այդ հարցերի համար։
referee.chat — նույն գաղափարը, փորձագիտական պնդումների համար