M/E23

Beweisassistenten werden mehr und mehr zu einem hilfreichen Tool für Mathematiker:innen und Informatiker:innen. Wir werden die Stunde nutzen, um die Grundlagen des Beweisassistenten Lean kennen zu lernen. Wer möchte, kann sich Lean gerne unter https://lean-lang.org/download/ installieren und den Vortrag interaktiv verfolgen. Den verwendeten Code werde ich einen Tag vor dem Vortrag unter https://github.com/StamesJames/lean-introduction-code veröffentlichen.

Christian Benedict Smit

Darmstadt