KoMa 94/AK Lean (proof assistant): Unterschied zwischen den Versionen
Die Seite wurde neu angelegt: „{{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 Bewe…“ |
FelixS (Diskussion | Beiträge) Keine Bearbeitungszusammenfassung |
||
| Zeile 3: | Zeile 3: | ||
|AK=AK Lean (proof assistant) | |AK=AK Lean (proof assistant) | ||
|AKS_Typ=Austausch | |AKS_Typ=Austausch | ||
|Initiator=Felix | |Initiator=Felix (Potsdam) | ||
|Dauer= | |Leitung=Felix (Potsdam) | ||
|Dauer=1h | |||
|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. | |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. | Ich denke es könnte auch Anwendung in der Lehre geben. | ||
Aktuelle Version vom 23. Mai 2026, 12:55 Uhr
| AK Lean (proof assistant) | |
|---|---|
| 94. KoMa in Essen | |
| Globaler AK: | AK Lean (proof assistant) |
| Typ: | Austausch |
| Track: | |
| Vorgeschlagen von: | Felix (Potsdam) |
| Leitung: | Felix (Potsdam) |
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
