Upcoming Talks and Events
Martin Dvořák: LEAN
| Monday, June 22, 2026, 11:00 | |
| FAV/NTIS, meeting room UN309 (third floor, blue part of the building). | |
| Lean is a functional language based on dependent type theory. Lean allows us to write programs and formally verify them, and we can also build mathematics in it, including non-constructive mathematics. Lean is highly ergonomic for people and, at the same time, Lean is useful for artificial intelligence: AI agents propose theorems and their proofs, and Lean determines which of them are correct. In this talk, we will see how to work with Lean interactively, what has already been done in Lean, and what AI can do in it. Martin Dvořák earned a B.A. in General Computer Science and an M.A. in Artificial Intelligence from the Faculty of Mathematics and Physics at Charles University. He went on to pursue his Ph.D. at the Institute of Science and Technology Austria. Terence Tao served as the external reviewer for his dissertation, Pursuit of Truth and Beauty in Lean 4. He is currently working as a postdoc at the Department of Mathematics, Faculty of Applied Sciences, University of West Bohemia in Pilsen. Martin Dvořák contributes to the Mathlib library and runs the Lean4anarchy Discord server. |
Name: Bavarian-Czech AI Summer School - AI and Industry
| 7-11 September 2026 | |
| Scientific Centre for AI and SuperTech (speinshart.ai), Speinshart, Bavaria | |
|
Call for participation: here Suitable especially for: undergraduate, graduate and doctoral students with interest in AI and industry Practical "hackathon": visual inspection of industrial seals Language: English Cost: Free of charge for participants (including travel, accommodation and full board) Registration deadline: 26 June 2026 (UWB students must register ALSO at the portal, ECTS departures, look for the offer called "Bavarian-Czech AI Summer School 2026 - AI and Industry") |
|
![]() |







