Titel: Kolloquium zur Masterarbeit mit dem Titel "Formalisierung von Aussagen über quadratische Formen"

Zusammenfassung: Konkret geht es um das Theorem von Legendre, also notwendige und zulängliche Bedingungen für die Lösbarkeit von $ax^2+by^2+cz^2=0$.
Ziel der Arbeit war es, einen Beweis dieses Theorems in den Lean Theorem Prover zu übertragen.
Daher wird die Beweisskizze vorgestellt und es gibt eine kurze Einführung zu Lean.