55 lines
2.1 KiB
Lean4
55 lines
2.1 KiB
Lean4
import VersoManual
|
|
import Manual.Meta
|
|
|
|
set_option pp.rawOnError true
|
|
set_option verso.docstring.allowMissing true
|
|
|
|
open Verso.Genre
|
|
open Verso.Genre.Manual.InlineLean
|
|
|
|
#doc (Manual) "Anhang: Lizenz und Hinweise" =>
|
|
%%%
|
|
htmlSplit := .never
|
|
tag := "anhang"
|
|
file := "anhang"
|
|
%%%
|
|
|
|
Dieser Anhang sagt, unter welchen Bedingungen Sie diese Notizen
|
|
weiterverwenden dürfen, und wie sie entstanden sind.
|
|
|
|
# Lizenz
|
|
|
|
Diese Kursnotizen stehen, genau wie das begleitende Skript _Algebra
|
|
und Zahlentheorie_, unter der Lizenz
|
|
[Creative Commons Namensnennung 4.0 International (CC BY 4.0)](https://creativecommons.org/licenses/by/4.0/deed.de).
|
|
|
|
Sie dürfen das Material also in jedem Format teilen und bearbeiten,
|
|
auch kommerziell, solange Sie angemessene Urheber- und Rechteangaben
|
|
machen, einen Link auf die Lizenz beifügen und angeben, ob Änderungen
|
|
vorgenommen wurden. Der vollständige Lizenztext liegt im Repository
|
|
in der Datei `LICENSE`.
|
|
|
|
Der zitierte Lean-Code lebt von [Mathlib](https://github.com/leanprover-community/mathlib4),
|
|
das seinerseits unter der Apache-Lizenz 2.0 steht. Die Namen der
|
|
zitierten Lemmata und Definitionen gehören dorthin, nicht hierher.
|
|
|
|
# Zur Entstehung: KI-Einsatz und Originalität
|
|
|
|
Diese Notizen sind unter starkem Einsatz von KI-Werkzeugen (großen
|
|
Sprachmodellen) entstanden. Das gilt für die Lean-Beweise ebenso wie
|
|
für die deutsche Prosa: Beides wurde weitgehend maschinell entworfen
|
|
und von mir anschließend geprüft, korrigiert und überarbeitet.
|
|
|
|
Ich erhebe daher *keinerlei Anspruch auf Originalität*. Die
|
|
Mathematik stammt aus der Vorlesung und ist Standardstoff; die
|
|
Beweisideen stammen aus dem Skript; die eigentliche Arbeit im Beweis
|
|
leisten die Lemmata aus Mathlib, die hier nur zusammengesetzt und
|
|
kommentiert werden. Der Beitrag dieser Notizen liegt allein in der
|
|
Auswahl und der Aufbereitung des Materials.
|
|
|
|
Ein Trost bleibt: Sämtlicher Lean-Code in diesen Notizen wird beim
|
|
Bauen des Buches mitelaboriert. Die gezeigten Beweise sind also vom
|
|
Compiler geprüft, ganz gleich, wer oder was sie geschrieben hat. Für
|
|
die Prosa gilt das nicht — Fehler darin gehen zu meinen Lasten.
|
|
Hinweise darauf nehme ich gerne entgegen.
|