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.

Nach meinem Mathematik-Studium an der TU Dortmund von 2000 bis 2005 und weiteren Stationen an der Universität arbeite ich seit 2012 in der IT-Beratung. Meine Kollegen und ich beantworten dort Kundenfragen der Form 'Sollen wir die Software einkaufen oder selbst programmieren? Was sollen wir programmieren? Wie können wir das Programmierte testen?'. Die im Studium gelernten Ergebnisse wie der Satz von Stokes, der Hilbertsche Nullstellensatz oder der Simplex-Algorithmus helfen uns hierbei nicht, sehr wohl aber die gelernten Fähigkeiten wie das Verstehen schwieriger Texte, das Argumentieren und das technische Schreiben. Im Vortrag möchte ich meinen Werdegang, die in unseren Projekten eingesetzten mathematischen Fähigkeiten und die Firma Consileon vorstellen.