Курс "Математичні доведення в Lean 4"

Іоргов Микола Зинонійович , заступник завідувача кафедри теоретичної та математичної фізики КАУ, з 14 вересня читатиме курс "Математичні доведення в Lean 4".

Lean 4 має розвинуту систему типів, яка дозволяє сформулювати математичні теореми та їх доведення як програми. Тому компілятор, коли перевіряє, що всі типи в програмі узгоджені, він фактично перевіряє коректність математичних доведень. Отже, якщо доведення, написане як програма в Lean 4, компілюється, значить доведення правильне.

В останній час, коли ШІ доводить математичні теореми, його змушують записати їх мовою Lean, щоб компілятор Lean зміг перевірити коректніть доведення.

Коли: Щопонеділка о 14:30
Де: Zoom
https://www.google.com/goto?url=CAESggEB6zswFc9kr4d6mgI3ps4_8Uz1RYJNoar5TDPGl3R6_7Q1xSC07bRNMHTbyrsoWjHw3juEVDxzdgBbsXSj6ea5H4PbdzsaaXS6EDbtSqv3NhhoQZybKq2atWLyI5atu-3Tp6jnfOPqYY2QeoYWm7LI8y5b0c_OBPTY-mVHzbXSjPko