Умовы выкарыстання
1. Што робіць сервіс
Вы падаеце заяву і стандарт. Мы прапускаем яго праз панэль мадэляў машыннага навучання, якія вы выбіраеце, плюс мадэль суддзі, якая вызначае крытэрый прыняцця, і мы спрабуем фармалізаваць вынік у Lean 4 супраць Mathlib. Вывад - гэта транскрыпцыя, набор рашэнняў, вердыкт, і, калі была спроба фармалізацыі, вынік Lean.
2. Што гэта за вывад і што не
Усе астатнія ўдзельнікі ўдзельнічаюць у спартыўных спаборніцтвах і не маюць права на ўдзел. Гэта не юрыдычная, медыцынская, фінансавая, інжынерная або прафесійная кансультацыя любога роду, і не створаны прафесійныя адносіны пры выкарыстанні гэтага сэрвісу.
Арбітр, які выносіць рашэнне па крытэру, які адпавядае крытэру, з' яўляецца заявай аб доказы ў запісе ў гэтай гульні. Гэта не гарантыя правільнасці. Мадэлі машыннага навучання робяць памылкі, няправільна чытаюць крыніцу і могуць выдумляць цытаты, нягледзячы на інструкцыі не рабіць гэтага. Вы павінны самастойна праверыць усё, на што вы хочаце разлічваць, асабліва перад апублікаваннем, перададзеннем або дзеяннем на яго. Гэта інструмент для праверкі працы, не замена для кваліфікаванага прагляду чалавекам.
Паспяховая формалізацыя Lean азначае, што ядра Lean прыняло доказ фармалізаванага выказвання ў адпаведнасці з версіяй Mathlib, якая выкарыстоўвалася ў той час. Гэта не азначае, што выказванне з' яўляецца дакладным перакладам таго, што вы запыталі, і выбар фармальнага выказвання, якое не кажа пра тое, што вы маеце на ўвазе, з' яўляецца найбольш распаўсюджаным спосабам увядзення ў зман формальных вынікаў. Прачытайце фармальнае выказванне, а не толькі вердыкт.
Ваш змест
Вы застаецеся ўладальнікам перададзеных вамі заявак і вынікаў, створаных для вас. Вы даяце нам толькі ліцэнзію, неабходную для працы сервісу: для апрацоўкі вашых заявак, перадачы іх выбраным вамі пастаўшчыкам мадэляў і захавання атрыманых адпаведнасцяў, каб вы маглі вярнуцца да іх.
Матчы па змаўчанні прыватныя. Калі вы пазначыце матч публічным, ён стане даступным для ўсіх, хто мае спасылку, і можа з' явіцца ў нашай публічнай галерэі. Не публікуйце матч, які змяшчае канфідэнцыйныя дадзеныя.
Не перадайце асабістыя дадзеныя пра іншых, канфідэнцыйныя матэрыялы, якія вы не маеце права распаўсюджваць, або змест, які з'яўляецца незаконным.
Крэдыты і рахункі
Крэдыт прадаплачаны і выкарыстоўваецца падчас гульні. Кожная гульня мае свой абмежаванне выдаткаў, якое вы вызначаеце; дасягненне гэтага абмежавання прыпыняе гульню, а не працягвае выдаткі. Баланс не пераносіцца і, акрамя выпадкаў, калі гэта патрабуецца законам, не вяртаецца пасля выкарыстання. Невыкарыстаны крэдыт можа быць вярнуты па патрабаванні.
Калі вы падлучыце свой уласны ключ, вы плаціце прадаўцу, і мы не патрабуем платы за токен. Пасля выкарыстання свабоднага месца на дыску будзе патрабавацца плаціць за інфраструктуру, каб забяспечыць працу панелі, інструментаў і сховішча.
Мы можам змяніць цэны без папярэджання. Змены не ўплываюць на ўжо набыты крэдыт.
Дазволенае выкарыстанне
Не выкарыстоўвайце сервіс для стварэння зместу, які шкодзіць іншым, для спробы атрымаць нашы запыты або сістэмныя інструкцыі, для абходу абмежаванняў выдаткаў або тарыфаў, або для перапродажу доступу без пісьмовага пагаднення. Праграма выканання кода прызначана для праверкі заяваў; не выкарыстоўвайце яе для атакі на любую сістэму.
Даступнасць
Мы залежым ад трэціх бакоў, якія прапануюць мадэлі. Прадстаўнікі не працуюць, змяняюць мадэлі і выкідваюць іх. Суадносіны, перарванае па якой- небудзь прычыне, прыпыняецца і працягваецца; мы не патрабуем платы за працу, якая не адбылася. Мы не гарантуем бесперабойную даступнасць, і мадэль, якую вы выкарыстоўвалі раней, можа стаць недаступнай.
Адказнасць
У поўнай меры, дазволенай законам, сэрвіс прадастаўляецца ў тым выглядзе, у якім ён ёсць, без гарантый любога роду. Наша агульная адказнасць за любыя прэтэнзіі абмяжоўваецца сумай, якую вы заплацілі нам за тры месяцы да ўзнікнення прэтэнзіі. Мы не нясем адказнасці за непасрэдныя або наступныя страты, уключаючы любыя страты, якія ўзнікаюць з- за даверу да вынікаў мадэлі.
Выкананне
Вы можаце закрыць свой рахунак у любы час; мы вернем невыкарыстаныя крэдыты. Мы можам прыпыніць рахункі, якія парушаюць гэтыя ўмовы або якія ставяць сервіс пад пагрозу.
Змены, мова і кантакт
Мы можам абнаўляць гэтыя ўмовы; матэрыяльныя змены будуць абвешчаныя на сайце.
Пераклад гэтай старонкі зроблены для зручнасці і аўтаматычна. Калі пераклад і англійская версія адрозніваюцца, англійская версія мае перавагу.
Пытанні: Звязацца з намі.