Lean (помощник по доказательствам)

Lean - это средство доказательства теорем и язык программирования . Он основан на исчислении конструкций с индуктивными типами .

Lean имеет ряд особенностей, которые отличают его от других интерактивных средств доказательства теорем. Lean может быть скомпилирован в JavaScript и доступен в веб-браузере. Он имеет встроенную поддержку символов Юникода. (Их можно набирать с использованием последовательностей, подобных LaTeX , таких как «\ times» вместо «×».) Lean использует свой собственный язык для метапрограммирования. Итак, если пользователь хочет написать функцию, которая автоматически доказывает некоторые теоремы, он пишет эту функцию на собственном языке Lean.

Lean привлек внимание математиков Томаса Хейлза ^[1] и Кевина Баззарда . ^[2] Хейлз использует его в своем проекте Formal Abstracts . Баззард использует его для проекта Зена . Одна из целей проекта «Зена» - переписать все теоремы и доказательства в программе бакалавриата по математике Имперского колледжа Лондона в Лин.

Примеры [ править ]

Вот как натуральные числа определяются в Lean.

индуктивный  нат  :  Тип |  ноль  :  нац |  succ  :  nat  →  nat

Вот операция сложения, определенная для натуральных чисел.

определение  add  :  nat  →  nat  →  nat |  n  ноль  : =  n |  n  ( succ  m )  : =  succ ( добавить  n  m )

Это простое доказательство в экономичном режиме.

Теорема  and_swap  :  р  ∧  д  →  д  ∧  р  : =  Предположим ,  h1  :  р  ∧  д ,  ⟨ h1.right ,  h1.left ⟩

Это же доказательство может быть выполнено с помощью тактики.

теорема  and_swap  ( p  q  :  Prop )  :  p  ∧  q  →  q  ∧  p  : = begin  Предположим, что  h  :  ( p  ∧  q ),  - предположим, что p ∧ q истинно в  случаях  h ,  - извлеките отдельные предложения из  расщепления конъюнкции ,  - разделить целевое соединение на два случая: доказать p и доказать q отдельно  повторить  {  предположение  } конец

См. Также [ править ]

• Помощник доказательства
• мималлок

Ссылки [ править ]

Внешние ссылки [ править ]

• Бережливый веб-сайт
• Игра с натуральными числами - интерактивное руководство по изучению бережливого производства