https://de.komapedia.org/api.php?action=feedcontributions&feedformat=atom&user=FelixS 2026-05-24T20:34:49Z Benutzerbeiträge MediaWiki 1.44.5 https://de.komapedia.org/index.php?title=KoMa_94/AK_Lean_(proof_assistant)&diff=24523 2026-05-23T12:55:23Z

<p>FelixS: </p> <hr /> <div>{{Vorlage:Arbeitskreis Session<br /> |Name=AK Lean (proof assistant)<br /> |AK=AK Lean (proof assistant)<br /> |AKS_Typ=Austausch<br /> |Initiator=Felix (Potsdam)<br /> |Leitung=Felix (Potsdam)<br /> |Dauer=1h<br /> |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.<br /> Ich denke es könnte auch Anwendung in der Lehre geben.<br /> Möglich wäre z.B. Skripte, Musterlösungen, etc. in Lean zu &quot;übersetzten&quot;. Die Beweise wäre dann mit einen sehr hohen Detailgrad vorhanden und das könnte ggf. beim Verständnis helfen. <br /> Grundsätzlich wäre der Aufwand hier enorm; aber mit (vernünftiger) Nutzung von LLMs wäre das vielleicht feasable.<br /> Aber natürlich müsste man die Studis dann auch noch Lean beibringen...<br /> Was haltet ihr von der Idee? Hab ihr schon Erfahrungen mit Lean4 gemacht?<br /> Lass uns darüber austauschen!<br /> Kommt auch gerne vorbei, wenn ihr findet, dass sich &quot;Proof Assistant&quot; interessant anhört :p<br /> }}</div>

FelixS