U utorak 16.06. u 14 časova u učionici 840 biće održano sledeće predavanje.

Predavač: Marcus Zibrowius, 

Professor of Topology and Geometry at Heinrich Heine University Düsseldorf.

Naslov predavanja: QED or Game Over? – A gamified introduction to theorem proving in Lean 

Apstrakt: The level of rigour mathematicians demand of a proof has increased steadily over the centuries. In the digital age, a complete formalization and algorithmic verification of proofs is likely to become the new standard. But what does such a formalization even look like? In this presentation, we will provide a brief introduction to the language Lean and its enormous mathematical library, which already covers huge chunks of university-level mathematics. All examples we will present are freely accessible via the Lean Game Server at https://adam.math.hhu.de, and you can verify each proof step live on your phone.