]> 2026-05-24T20:10:53+00:00 KoMa 94/AK Lean (proof assistant) 0 de 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 AK Lean (proof assistant) Austausch 1h Felix (Potsdam) 94 Felix (Potsdam) KoMa 94/AK Lean (proof assistant) 2026-05-23T12:55:23Z 2461184.0384607 KoMa 94/AK Lean (proof assistant) 0 0 plainlist 1 [[:KoMa 94]] KoMa 94/AK Lean (proof assistant)# QUERY7bb3200536e62273e9b587a5174e27d3 0 0 plainlist 1 [[:KoMa 94/AK Lean (proof assistant)]] KoMa 94/AK Lean (proof assistant)# QUERYf3db411a4c8b1e970e84d150d98ee748 0 1 plainlist 5 [[Kategorie:Arbeitskreis Session]] [[KoMaNr::94]] [[AKS Name::AK Lean (proof assistant)]] KoMa 94/AK Lean (proof assistant)# QUERY8d50becf966e3320de6237ee8097ce1a 0 1 plainlist 3 [[Kategorie:KoMa]] [[KoMaNr::94]] KoMa 94/AK Lean (proof assistant)# QUERYbfc65b21f5318c5febd8819e1df282ef