Welcher Fehler ist ein trivialer Irrtum?

Wenn sich ein Fehler in einer Definition oder einem Beweis zwar leicht beheben lässt, aber schwer zu entdecken ist, dann ist dieser Irrtum nicht trivial.
Manche Fehler lassen sich nur mithilfe eines Proof Assistants finden.

Von letztem Dezember bis zum 16. April dieses Jahres habe ich rund 170 Stunden darauf verwendet, den String-Theorem String.splitOn_of_valid in der Standardbibliothek des Lean-Proof-Assistants zu beweisen.
Während ich dieses Theorem bewies, entdeckte ich einen Bug in der Definition der Funktion String.splitOn.
Diesen Bug zu beheben war nicht besonders schwierig. In der betreffenden Definition musste lediglich i durch i - j ersetzt werden.
Trotzdem halte ich diesen Fehler nicht für einen trivialen Irrtum. Nach dieser Definition funktioniert die Funktion splitOn meist korrekt, liefert aber in Sonderfällen ein falsches Ergebnis.
Ohne einen Proof Assistant wie Lean hätte ich einen derart subtilen Fehler niemals finden können.

Verwandte Beiträge