Андрій Севастьянов пояснює, як математичні доведення можна записати у вигляді коду в мові програмування Lean 4.

У статті про те, чому мова для цього не може бути Т'юрінг-повною, що таке структурна рекурсія та залежні типи і як на практиці працює ізоморфізм Каррі — Говарда.

👉 https://dou.ua/goto/6jKN