Друзі, є цікава новина:

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

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

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

До заняття можна буде підключитися по Zoom (щопонеділка о 14:30). Також планується запис лекцій.