У уторак 16.06. у 14 часова у учионици 840 биће одржано следеће предавање.

Предавач: Marcus Zibrowius, 

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

Наслов предавања: QED or Game Over? – A gamified introduction to theorem proving in Lean 

Апстракт: 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.