لین (دستیار اثبات)

**لین  (Lean)** یک دستیار اثبات و یک زبان برنامه‌نویسی تابعی است. این زبان مبتنی بر حساب سازه‌ها با نوع‌های القایی است. Lean یک پروژه متن‌باز است که بر روی گیت‌هاب میزبانی می‌شود. این زبان به طور اولیه توسط لئوناردو د مورا در حین اشتغال در مایکروسافت ریسرچ توسعه داده شد و اکنون در آمازون وب سرویسز ادامه دارد. توسعه این زبان در حال حاضر توسط سازمان Lean سازمان تحقیقات متمرکز (FRO) پشتیبانی می‌شود.

## تاریخچه
لین  توسط لئوناردو د مورا در مایکروسافت ریسرچ در سال ۲۰۱۳ راه‌اندازی شد. نسخه‌های اولیه این زبان، که بعدها به نام Lean 1 و 2 شناخته شدند، آزمایشی بودند و ویژگی‌هایی مانند پشتیبانی از نظریه نوع هموتوپی داشتند که بعدها حذف شدند.

Lean 3 (برای اولین بار در ۲۰ ژانویه ۲۰۱۷ منتشر شد) اولین نسخه نسبتاً پایدار Lean بود. این نسخه عمدتاً با زبان C++ پیاده‌سازی شده بود و برخی از ویژگی‌ها نیز با خود زبان Lean نوشته شده بودند. پس از نسخه 3.4.2، Lean 3 به طور رسمی پایان عمر خود را اعلام کرد در حالی که توسعه Lean 4 آغاز شد. در این دوره بینابینی، اعضای جامعه Lean نسخه‌های غیررسمی تا 3.51.1 را توسعه داده و منتشر کردند.

در سال ۲۰۲۱، Lean 4 منتشر شد که بازسازی اثبات‌گر Lean بود که قادر به تولید کد C است که سپس کامپایل می‌شود و امکان توسعه خودکارسازی حوزه‌های خاص را فراهم می‌کند. Lean 4 همچنین سیستم ماکرو و بهبودهای سنتز کلاس نوع و روش‌های مدیریت حافظه را نسبت به نسخه قبلی داراست. یکی دیگر از مزایای آن نسبت به Lean 3، امکان اجتناب از لمس کد C++ برای تغییر رابط کاربری و دیگر قسمت‌های اصلی سیستم است، زیرا همه آنها اکنون در Lean پیاده‌سازی شده و در دسترس کاربر نهایی برای جایگزینی در صورت نیاز هستند.

Lean 4 با Lean 3 سازگاری معکوس ندارد.

در سال ۲۰۲۳، Lean FRO تشکیل شد، با اهداف بهبود مقیاس‌پذیری و قابلیت استفاده از زبان و اجرای اتوماسیون اثبات.

## مرور کلی
### کتابخانه‌ها

بسته رسمی لین شامل یک کتابخانه استاندارد *std4* است که ساختارهای داده‌ای مشترک را که می‌تواند برای هر دو تحقیق ریاضی و توسعه نرم‌افزار متعارف استفاده شود، پیاده‌سازی می‌کند.

در سال ۲۰۱۷، یک پروژه نگهداری شده توسط جامعه برای توسعه یک کتابخانه Lean *mathlib* آغاز شد، با هدف دیجیتالی کردن هر چه بیشتر ریاضیات ریاضیات محض در یک کتابخانه بزرگ یکپارچه، تا سطح تحقیقاتی ریاضی. تا نوامبر ۲۰۲۳، mathlib بیش از ۱۲۷,۰۰۰ قضیه و ۷۰,۰۰۰ تعریف را در Lean رسمی کرده بود.

### یکپارچه‌سازی ویرایشگرها

لین  با: 

* ویژوال استودیو کد
* نئو ویم
* ایمکس

ارتباط‌گیری از طریق یک سرور پروتکل زبان و یک افزونه کلاینت انجام می‌شود.

این زبان دارای پشتیبانی بومی از نمادهای یونیکد است که می‌توان با استفاده از توالی‌های شبیه به LaTeX، مانند "\times" برای "×" تایپ کرد. Lean همچنین می‌تواند به جاوااسکریپت کامپایل شود و در یک مرورگر وب دسترسی داشته باشد و از پشتیبانی گسترده‌ای برای فرا-برنامه‌نویسی برخوردار است.

## نمونه‌ها (Lean 4)

اعداد طبیعی می‌توانند به عنوان یک نوع القایی تعریف شوند. این تعریف بر اساس اصل پیانو است و بیان می‌کند که هر عدد طبیعی یا صفر است یا جانشین عدد طبیعی دیگری است.

```lean
inductive Nat : Type
| zero : Nat
| succ : Nat → Nat
```


جمع اعداد طبیعی می‌تواند به صورت تعریف بازگشتی تعریف شود، با استفاده از تطبیق الگو.

```lean
def Nat.add : Nat → Nat → Nat
| a, zero => a
| a, succ b => succ (Nat.add a b)
```


با استفاده از این تعریف‌ها، ما می‌توانیم یک اثبات تعریف بازگشتی برای یک قضیه ساده بنویسیم.

```lean
theorem zero_add (a : Nat) : Nat.add zero a = a :=
  match a with
  | zero => rfl
  | succ a' => congrArg succ (zero_add a')
```


## منابع

## پیوند به بیرون
* Lean Website
* Lean Community Website
* Lean FRO
* The Natural Number Game - an interactive tutorial to learn Lean
* Moogle.ai - a semantic search engine for finding theorems in mathlib

رده:دستیارهای اثباتی
رده:زبان‌های تابعی
رده:سیستم‌های نرم‌افزاری اثبات قضیه
رده:مؤسسه تحقیقاتی مایکروسافت
رده:نرم‌افزار آزاد و متن‌باز
رده:نرم‌افزارهای آزاد نوشته‌شده با سی++
رده:نرم‌افزارهای آموزشی ریاضی
رده:نرم‌افزارهای رایگان مایکروسافت
رده:نرم‌افزارهای ریاضی آزاد
رده:نرم‌افزارهایی که از پروانه آپاچی استفاده می‌کنند