Bearbeiten von „KoMa 94/AK Lean (proof assistant)“

{{Vorlage:Arbeitskreis Session
|Name=AK Lean (proof assistant)
|AK=AK Lean (proof assistant)
|AKS_Typ=Austausch
|Initiator=Felix
|Dauer=~45min
|AKS_Kurzbeschreibung=In Potsdam läuft aktuell ein recht formloses Seminar, wo Personen aus dem Kollegium, und vereinzelt auch Studis, versuchen zusammen Lean4 zu lernen.
Ich denke es könnte auch Anwendung in der Lehre geben.
Möglich wäre z.B. Skripte, Musterlösungen, etc. in Lean zu "übersetzten". Die Beweise wäre dann mit einen sehr hohen Detailgrad vorhanden und das könnte ggf. beim Verständnis helfen. 
Grundsätzlich wäre der Aufwand hier enorm; aber mit (vernünftiger) Nutzung von LLMs wäre das vielleicht feasable.
Aber natürlich müsste man die Studis dann auch noch Lean beibringen...
Was haltet ihr von der Idee? Hab ihr schon Erfahrungen mit Lean4 gemacht?
Lass uns darüber austauschen!
Kommt auch gerne vorbei, wenn ihr findet, dass sich "Proof Assistant" interessant anhört :p
}}