Арық (көмекші көмекші) - Lean (proof assistant) - Wikipedia

Арық (көмекші көмекші)
ӘзірлеушілерMicrosoft Research
Бастапқы шығарылым2013; 7 жыл бұрын (2013)
Тұрақты шығарылым
3.4.2 / 18 қаңтар 2019 ж; 23 ай бұрын (2019-01-18)
Репозиторийgithub.com/ leanprover/сүйену
ЖазылғанC ++
Операциялық жүйеКросс-платформа
Қол жетімдіАғылшын
ТүріДәлелдеу көмекшісі
ЛицензияApache лицензиясы 2.0
Веб-сайтleanprover.github.io

Сүйену Бұл теоремалық мақал және бағдарламалау тілі. Ол негізделеді Құрылыстардың есебі бірге индуктивті түрлері.

Lean-дің басқа интерактивті теорема провайдерлерінен ерекшеленетін бірқатар ерекшеліктері бар. Lean-ді JavaScript-ке жинауға болады және оған веб-шолғышта кіруге болады. Онда Unicode символдары үшін жергілікті қолдау бар. (Оларды пайдаланып теруге болады LaTeX «× times» сияқты « times» сияқты тізбектер.) Lean мета-бағдарламалау үшін өзінің тілін қолданады. Сонымен, егер пайдаланушы кейбір теоремаларды автоматты түрде дәлелдейтін функцияны жазғысы келсе, олар сол функцияны Lean-дің өз тілінде жазады.

Lean математиктердің назарын аударды Томас Хейлс[1] және Кевин Баззард.[2] Хейлс оны өз жобасы үшін пайдаланады, Ресми тезистер. Баззард оны үшін қолданады Xena жобасы. Xena жобасының мақсаттарының бірі - студенттердің математикаға арналған оқу бағдарламасындағы барлық теоремалар мен дәлелдерді қайта жазу. Лондон императорлық колледжі арықта.

Мысалдар

Lean-де натурал сандар қалай анықталады.

индуктивті нат : Түрі| нөл : нат| сук : нат → нат

Мұнда натурал сандар үшін анықталған қосу әрекеті келтірілген.

анықтама қосу : нат → нат → нат| n нөл     := n| n (сук м) := сук(қосу n м)

Бұл терминдік режимде үйренудің қарапайым дәлелі.

теорема және ауыстыру : б ∧ q → q ∧ б :=    болжау h1 : б ∧ q,    ⟨h1.оң, h1.сол⟩

Дәлелді тактиканы қолдану арқылы да жасауға болады.

теорема және ауыстыру (б q : Тірек) : б ∧ q → q ∧ б :=баста    болжау сағ : (б ∧ q), - p ∧ q дұрыс деп қабылдаңыз    істер сағ, - жалғаулықтан жеке ұсыныстарды бөліп алу    Сызат, - мақсат конъюнкциясын екі жағдайға бөлу: p-ны дәлдеу және q-ны бөлек дәлелдеу    қайталау { болжам }Соңы

Сондай-ақ қараңыз

Әдебиеттер тізімі

  1. ^ Хэйлс, Томас. «Арық теореманы дәлелдеушіге шолу». Алынған 6 қазан 2020.
  2. ^ Баззард, Кевин. «Математиканың болашағы?» (PDF). Алынған 6 қазан 2020.

Сыртқы сілтемелер