About Theorem.chat
Theorem.chat математик таләпне ала һәм аны хәл итәргә тырыша. Сез таләпне һәм аның үтәргә тиешле стандартны күрсәтәсез. Хайван акылы модельләре төркеме - сез теләгәнчә күп, теләсә кайсы сатучыдан - аны һөҗүм итә, һәм тагын бер модель хөкемдар. Соңыннан аргумент Lean 4 белән Mathlib арасында формалаштырыла, һәм Lean ядрәсе аны раслауны яки расламауны хәл итә. Соңгы адым продукт.
Ни өчен башка модель урынына үзәк
Модельгә катлаулы сорау бирегез һәм дөресме-юкмы дигән сорауга төгәл җавап бирерсез. Берничә сорау бирегез һәм алар еш кына килешерләр, бу дөресме-юкмы дигән сорауга җавап бирү кебек тоела, ләкин бу шулай түгел: модельләр өйрәтү мәгълүматларын һәм күрмәүче урыннарын уртаклашалар. Икенче модель беренчесен тикшерә, бу да шул ук фикерләү, һәм бу турында сөйләшергә мөмкин. Леан ядрәсе бу эшне эшли алмый. Ул яки аксиомалардан һәм Mathlibдән белдерүне ала, яки юк, һәм ышаныч нәтиҗәгә йогынты ясамый.
Формаль дәлилне ялганлауның гадәти ысуллары тикшерелә һәм кире кагыла. sorry белән бушлык калдырган дәлил, native_decide-гә мөрәҗәгать итеп үзәкне ышанычлы исәпләүне кабул итәргә мәҗбүр иткән яки яңа аксиоманы тыныч кына керткән дәлил, табыла һәм уңышлы дип исәпләнмичә кире кагыла.
Панельнең чынлыкта нәрсә эшли алуы
Аргументлар бирү җиңелрәк. Панель arXiv, OpenAlex, Crossref кебек әдәбият белән эшли, шуңа күрә билгеле нәтиҗәләр начар итеп яңадан китереп чыгарылмыйча гына китерелә. Анда SageMath һәм PARI/GP исәпләү өчен, Z3 һәм CVC5 SMT чишү өчен, OEIS эзләү өчен төзелгән җепне ачыклау өчен, һәм Python тирәлегенең челтәргә керү мөмкинлеге булмаган sandboxы бар. Берәр кеше аны раслау өчен бер уен уйнаганчы, фаразны 10 мең очрак белән тикшерергә мөмкин, һәм каршы мисал фикер алышуны тиз арада тәмамлар.
Әтисе — Әхмәтҗан, әнисе — Мәрьям.
Согласование аргумент сыйфаты буенча бәяләнми. Согласование таләпләре кабул итү критерийларына бүленә, һәм критерий бары тик аның артында нәрсәдер өченче як тарафыннан тикшерелгәндә генә хәл ителә: кирәкле җөмлә белән китерелгән чыганак, яки чынлап та башкарылган код аның чын чыганагы белән. Рефери карар чыгарыр алдыннан үзенең дәлилләрен үзе тикшерә, һәм критерий ачык булганда, ул согласованиене тәмамланган дип игълан итә алмый.
Сез чикне куясыз
Стандартны үзегезгә сайларга туры килә, ә арбитр аны сүз белән генә тота. Тиздән эксперт кабул итәр дип көтегез һәм сез аны алачаксыз. Һәрбер фараз белән тулы дедуктив аргументны сорагыз һәм сез аның урынына шуның белән хөкем ителәсез. Премия тапшыру өчен бармакны сорагыз, һәм чын нәтиҗә гадәттә панельнең кайбер өлешләрендә кимчелек булуын төгәл аңлата - бу сезнең үзегез тикшерергә тиеш булган ышанычлы белдерүдән күбрәк бәягә ия.
Бу хакта ачык итеп әйтим: бу машина ачык проблемаларны хәл итүче машина түгел. Бу машина аргументны хәл ителгән дип кабул итүдән баш тарта, әгәр ул хәл ителмәгән булса, һәм ул сезгә төгәл генә кайсы адым хаталанганын әйтә.
Формальләштерү хатасы файдалы чыганак
Әгәр Lean исбатлауны ябып бетерә алмаса, калган максатны табасыз. Практикада бу һәрвакытта да формаль аргументның кул чабу урыны була - бу адым һәркемнең проза версиясен укыган вакытта башларын иеп үтүе булыр иде. Бу максат соңыннан аны һөҗүм итү өчен иң яхшы урынга тапшырыла, инде уйлап каралган нәрсә белән бергә, һәм башка берни дә юк. Моделләр, алар ябык булса, үзләрен бөтен чыгымнар белән кабатлап, бушап калалар; бер конкрет сорауны үтәү урынына, гадәттә, блокировканы бушатып, уенчылар санының бер өлешен ала.
Күп вакытлы эш
Панель төзегән һәрбер грамматик берәмлек үзенең дәлилләре белән уртак бухгалтериягә керә, шуңа күрә нәтиҗәләр бер тапкыр гына языла һәм беркайчан да яңадан китерелә алмый, һәм буш урыннар теркәлә, шуңа күрә алар янына беркем дә кайтмый. Согласование сервер ягында бара һәм чиста тукталыш белән тәмамлана - бюджет буенча, провайдер тукталыш белән яки сез битне ябып куйган өчен - һәм туктаган урыныннан төгәл дәвам итә.
Бу нәрсә өчен түгел
Теорема - бу дедуктив сүз. Бу сайт математика, логика, теорияле компьютер фәне, теорияле физика һәм икътисад теориясе өчен төзелгән - бу өлкәләрдә исбатлау белән хәл ителә торган сораулар. Биология, медицина, химия яки җәмгыять фәннәре өлкәсендә эмпирик сораулар теоремаларны китереп чыгармый, алар нәтиҗәләр китереп чыгара, һәм аларны формальләштерү күләме аларны хәл итә алмаячак. Безнең туган сайтыбыз referee.chat шул ук сорауларга Lean адымсыз да, шул ук панель- һәм рефери процессын эшли.