Eine ontologische Re-Interpretation offener Quantensysteme?!

[antaris]

Das ist falsch.

Eine Komplexifizierung ausgehend von GL(R) liefert lediglich GL(C); das liefert keine Hermitizität, die musst du zusätzlich fordern.

Interessant.


-- Definitionen:
-- fullHamiltonian L := fun i j => (L i j : ℂ) -- Komplexifizierung
-- Matrix.IsHermitian H := conjTranspose H = H -- aus Mathlib

Original code:
/-- If `L` is symmetric over `ℝ`, then its complexification is Hermitian. -/
theorem fullHamiltonian_isHermitian_of_transpose_eq
(L : Matrix Ω Ω ℝ) (hL : Matrix.transpose L = L) :
Matrix.IsHermitian (fullHamiltonian (Ω := Ω) L) := by
classical
dsimp [Matrix.IsHermitian, fullHamiltonian]
ext i j
have hij : L j i = L i j := by
have h := congrArg (fun M : Matrix Ω Ω ℝ => M i j) hL
simpa [Matrix.transpose_apply] using h
-- `conj` fixes real scalars; transpose symmetry gives Hermitian symmetry
simp [Matrix.conjTranspose_apply, hij]


Korrekt ist die kanonische Einbettung ℝ ↪ ℂ, Eintrag für Eintrag. Die Hermitizität folgt dann aus der zusätzlich geforderten Hypothese L^T = L, die im Theorem als hL explizit drinsteht.
Nur der Kommentar ist falsch und ggf. bei den vielen Iterationen bei der Codeerstellung nicht mehr aktualisiert worden. Kommentare in lean sind halt auch nur prosa.


Korrekt wäre der folgende Kommentar:

/-- If `L` is symmetric over `ℝ`, then its canonical embedding into `Mat(Ω, ℂ)` is Hermitian. -/


Das bedeutet ich kann den Kommentaren im code nicht vertrauen. Der code ist aber nach wie vor korrekt. Lean würde nicht kompilieren, wenn dem nicht so wäre. Das bedeutet aber auch, dass die Kommentare selbst ein Problem bei der Übersetzung in formalen code sind. Die AI muss viel mehr den code übersetzen und möglichst gar nicht die Kommentare auswerten.

 

[ralfkannenberg]

dieser code generiert oder prüft keine ISIN-codes. Das ist ein fehlerfreier -> kompilierter lean-Beweis mit dem Ziel "* The theorem proves that the computed check digit always verifies."

Hallo Antaris,

das verstehe ich nicht: ich habe einen Code für die Prüfziffer n von 20000 ISIN's benötigt und das Ergebnis ist dann eine einstellige Zahl, die anhand eines "erweiterten" Luhn-Algorithmus, den ich selber erraten musste, weil er im Internet falsch spezifiziert war, ermittelt wird.

Da brauche ich nichts anderes, nicht "verifies" oder was auch immer, sondern 20000 Prüfziffern, nämlich pro Raw-ISIN eine.


Freundliche Grüsse, Ralf

 

[antaris]

Hallo Ralf,

das verstehe ich nicht:

ich hatte ChatGPT aufgefordert einen lean-Beweis zu schreiben, der beweist, dass die berechnete Prüüfziffer immer korrekt ist.




Genauer, erklärt von claude:

Der Code ist eine formale Verifikation des ISIN/Luhn-Prüfziffern-Algorithmus in Lean 4 (mit der Mathlib-Bibliothek).

Was ist das Ziel? Es wird mathematisch bewiesen, dass die berechnete Prüfziffer einer ISIN (International Securities Identification Number) immer korrekt ist – also dass computeCheckDigit und verify konsistent zusammenarbeiten.

Die einzelnen Bausteine:

Der Code definiert zunächst die Kernfunktionen des Luhn-Algorithmus: dblAdjust verdoppelt eine Ziffer und zieht 9 ab, falls das Ergebnis ≥ 10 ist. altSum bildet eine alternierende Summe über eine Ziffernliste, wobei jede zweite Ziffer durch dblAdjust geschickt wird. computeCheckDigit berechnet die Prüfziffer so, dass die Gesamtsumme durch 10 teilbar wird, und verify prüft genau das.

Der Beweis läuft in mehreren Schritten: Zuerst wird gezeigt, dass die Luhn-Summe über payload ++ [checkDigit] sich sauber in payloadSum + checkDigit zerlegen lässt (Lemma fullSum_eq_payload_plus_check). Dann wird bewiesen, dass s + (10 - s % 10) % 10 immer durch 10 teilbar ist (Lemma mod_add_checkDigit). Zusammen ergibt das den Hauptsatz verify_compute_eq_true: Für jede Ziffernliste liefert verify mit der berechneten Prüfziffer immer true.

Am Ende gibt es einen konkreten Regressionstest mit der Apple-ISIN (US0378331005), bei dem Lean per decide automatisch nachrechnet, dass die Prüfziffer 5 ist und die Verifikation aufgeht.

Kurz gesagt: Der Code beweist nicht nur durch Tests, sondern mathematisch für alle möglichen Eingaben, dass die Prüfziffernberechnung korrekt ist.

 

[antaris]

Das bedeutet ich kann den Kommentaren im code nicht vertrauen. Der code ist aber nach wie vor korrekt. Lean würde nicht kompilieren, wenn dem nicht so wäre. Das bedeutet aber auch, dass die Kommentare selbst ein Problem bei der Übersetzung in formalen code sind. Die AI muss viel mehr den code übersetzen und möglichst gar nicht die Kommentare auswerten.

Ich habe das gerade mit ChatGPT getestet. Syntaktisch wurde der Beweis richtig wiedergegeben aber semantisch auch falsch in Prosa beschrieben. Ich habe bei ChatGPT in den Erinnerungen jetzt abgespeichert, dass Kommentare niemals ungeprüft gegen den kommentierten und fehlerfrei kompilierten code übernommen werden dürfen und auf die GFehler hingewiesen werden muss. Ob die AI derartige Fehler nur dadurch immer erkennen wird, ist zu bezweifeln. Zumindest ist es ein Problem, was nicht unlösbar ist. Es müssen halt alle Kommentare überprüft und ggf. korrigiert werden.

Die Antwort von ChatGPT, nachdem ich den Hinweis auf den falschen Kommentar: https://chatgpt.com/s/t_69c5963072348191a5330d25e21b692e
Obwohl der code da ist, nutzen AI's wohl dennoch eher menschliche Sprache, anstelle des für die Maschinen eigentlich viel verständlichere code. Das hat ChatGPT und claude gleichermaßen falsch gemacht.

 

[ralfkannenberg]

ich hatte ChatGPT aufgefordert einen lean-Beweis zu schreiben, der beweist, dass die berechnete Prüüfziffer immer korrekt ist.

Hallo Antaris,

aber das war doch gar nicht die Aufgabenstellung ...

Du siehst also, wie wichtig es ist, das zu beweisen, was man beweisen will und nicht irgendetwas anderes.

Zudem überrascht mich das Ergebnis, denn bei der ISIN muss man nicht von rechts nach links durchzählen, sondern von links nach rechts.


Freundliche Grüsse, Ralf

 

[antaris]

Hallo Ralf,

aber das war doch gar nicht die Aufgabenstellung ...

ja aber es hatte mich interessiert.

 

[antaris]

Zudem überrascht mich das Ergebnis, denn bei der ISIN muss man nicht von rechts nach links durchzählen, sondern von links nach rechts.

Antwort claude:

Das ist eine berechtigte Beobachtung, aber der Code macht es tatsächlich bereits korrekt – und zwar von links nach rechts.

Was der Code tut: Die Funktion altSum iteriert die Liste von links nach rechts und toggelt dabei das Bool-Flag b bei jedem Schritt. Die entscheidende Frage ist nur: Wird die erste Ziffer verdoppelt oder nicht? Das bestimmt payloadStart.

Der Unterschied zum "klassischen" Luhn: Beim Kreditkarten-Luhn zählt man von rechts nach links, wobei die Prüfziffer (ganz rechts) nicht verdoppelt wird und die zweite von rechts schon. Bei der ISIN wird dagegen von links nach rechts gezählt – aber welche Positionen verdoppelt werden, ist am Ende dasselbe, weil es nur darauf ankommt, welche Ziffern auf geraden bzw. ungeraden Positionen liegen.

Wie der Code das löst: payloadStart berechnet anhand der Länge des Payloads das korrekte Startflag, sodass nach dem Anhängen der Prüfziffer die Paritäten stimmen. Konkret: xs.length % 2 = 1 sorgt dafür, dass die Prüfziffer (letzte Position) nicht verdoppelt wird und alle anderen Positionen die richtige Zuordnung haben – und zwar bei Links-nach-rechts-Durchlauf.

Mathematisch ist das Ergebnis identisch, egal ob man von links oder rechts zählt – es kommt nur darauf an, dass die richtigen Positionen verdoppelt werden. Der Code formalisiert das richtungsunabhängig über die Längenparität, verarbeitet aber tatsächlich von links nach rechts, ganz im Sinne der ISIN-Spezifikation.

 

[ralfkannenberg]

ich würde ja jetzt den Formalismus zur Berechnung/Überprüfung der ISIN, inkl. Regressionstest, z.B. mit Python von der AI erstellen lassen und zusätzlich, mit Kanonen auf Spatzen schießend, das dann noch mit lean beweisen lassen.

Warum ist Probieren eine Schande?

aber das war doch gar nicht die Aufgabenstellung ...

ja aber es hatte mich interessiert.

Hallo Antaris,

das ist ja gut und recht, aber das musst Du doch hinschreiben. Woher kann ich denn wissen, dass Dich etwas ganz anderes interessiert, wenn Du das nicht aufschreibst ?

Das wäre übrigens einfach vermeidbar gewesen, wenn Du - worum Tom schon gebeten hat - genau aufschreiben würdest, was beweisen werden soll und was bewiesen worden ist.


Freundliche Grüsse, Ralf

 

[ralfkannenberg]

Mathematisch ist das Ergebnis identisch, egal ob man von links oder rechts zählt – es kommt nur darauf an, dass die richtigen Positionen verdoppelt werden. Der Code formalisiert das richtungsunabhängig über die Längenparität, verarbeitet aber tatsächlich von links nach rechts, ganz im Sinne der ISIN-Spezifikation.

Hallo Antaris,

das folgt trivialerweise aus Symmetriegründen.

Dennoch hilft es mir bei der Arbeit nicht weiter, wenn die Prüfziffern "falsch" herum ermittelt werden, denn dann kann ich für 20000 erstellte neue Wertpapiere ein Korrektur-Skript beantragen, um das wieder richtigzustellen.


Freundliche Grüsse, Ralf

 

[TomS]

Die Hermitizität folgt dann aus der zusätzlich geforderten Hypothese L^T = L, die im Theorem als hL explizit drinsteht.

Das ist auch falsch – das liefert keine Hermitizität, die musst du zusätzlich und insbs. anders fordern.

Komplexifizierung

Für L betrachtet man den Vektorraum V = V(R) der reellen Matrizen. Dann ist die Komplexifizierung

V(C) = V ⊕ iV

also die direkte Summe zweier Kopien des selben Vektorraumes V, mit den Vektoren v aus V(C) gemäß

v = v₁ ⊗ 1 + i ⊗ v₂ = v₁ + iv₂

wobei wobei v₁, v₂ die Vektoren aus V = V(R) sind. Letzteres ist die übliche Notation, die für jedes Matrixelement direkt auf z = x + iy führt. In deinem Fall wäre das

H = L₁ ⊗ 1 + i ⊗ L₂ = L₁ + iL₂

Aber deine Zusatzforderung L = L^T symmetrischer Matrizen darf nicht auf den zweiten reellen Vektorraum übertragen werden.

Hermitizität

Für H* = H benötigst du stattdessen

L₁^T = L₁
L₂^T = -L₂

wobei die zweite Forderung neu ist und nicht aus der Komplexifizierung folgt. D.h., entweder überträgst du die Forderung der Symmetrie auf den zweiten Vektorraum und erhältst nicht die gewünschte Hermitizät, oder du führst die neue Forderung der Antisymmetrie ein, erhälst die Hermitizät, wobei dies aber nicht aus der ursprünglich geforderten Zusatzbedingung für den reellen Vektorraum folgt.

Hermitizität folgt dann aus der zusätzlich geforderten Hypothese L^T = L, die im Theorem als hL explizit drinsteht.

Komplexifizierung garantiert keine Hermitizität, Komplexifizierung ist kein Theorem, und sie steckt nicht als Hypothese drin.

Deine Ausgangsbedingung ist der Vektorraum reeller Matrizen; damit kannst du aber den Vektorraum der hermetischen Matrizen nicht "beweisen" – du kannst ihn nur definieren, in dem du etwas Neues einführst. Wenn du die o.g. Forderung der Symmetrie bzw. Antisymmetrie (neu) auf dem ersten bzw. zweiten Vektorraum mittels einer Definition einführst, dann kannst du die Hypothese der Hermitizität einführen und beweisen. Definition und Beweis sind aber zwei völlig verschiedene Paar Schuhe.

Und deswegen reite ich so auf der Struktur Definition – Voraussetzung – Satz – Beweis herum. Du musst dir zuerst über die Struktur deiner Gedanken klar sein, erst danach kannst du die Software sinnvoll befüttern.

 

[TomS]

Das soll heißen

Komplexifizierung garantiert keine Hermitizität, Komplexifizierung ist kein Theorem, Hermitizität steckt nicht als Hypothese drin.

 

[antaris]

@TomS
Du hast vollkommen recht aber die Aussage des lean-Beweis ist eine andere.
Ich würde vorschlagen die Diskussion zu pausieren, solange das Problem mit den Kommentaren im code noch besteht.
Man kann in den Kommentaren teilweise klar erkennen, dass bei Änderungen der Syntaktik des codes die Semantik der Kommentare nicht mitgezogen wurde. Ich überarbeite das erstmal, bevor nur deswegen noch mehr Missverständnisse aufkommen. Das dauert ein wenig aber ich werde im strikten Pfad anfangen. Das sind "nur" 136 Module.

 

[antaris]

Ich überarbeite das erstmal, bevor nur deswegen noch mehr Missverständnisse aufkommen.

Im gesamten Repo liegen 270 Lean-Module, mit insgesamt 33 472 Zeilen. Es gibt dort 1 420 Docstrings (/--), 366 Modul-Dokblöcke (/-!), 690 Zeilenkommentare und 54 weitere Blockkommentare. Da ist allein die Überprüfung schon ziemlich aufwändig.
Die AI selbst muss irgendwas interpretieren, wenn ein Kommentar erstellt wird und das wird wahrscheinlich sehr schwer werden.

Aber ich habe einen Plan der funktionieren könnte aber wahrscheinlich einige Iterationen benötigt. Wie ich nun verstanden habe sollte das zentrale Objekt der "Zurschaustellung" immer die abstrakte Mathematik und möglichst keine Interpretationen/Narrative enthalten. Das Ziel ist Eindeutigkeit in den Kommentaren herzustellen und das geht nur, in dem direkt in den Kommentaren in formale Schrift übersetzt wird. Da es sich um einen code handelt, der mathlib nutzt, werde ich nun vollständig die öffentlich verfügbaren Docs für lean/mathlib übernehmen. Da steht alles formal beschrieben bzw. sozusagen vom code in formale Sprache übersetzt. Das ist dann vollständig auditierbar und zitierbar, fast schon so eine harte Leitplanke, wie lean selbst.
Ich glaube nur so kann es was werden.

 

[ralfkannenberg]

Ich glaube nur so kann es was werden.

Hallo Antaris,

wie gelingt es Dir, eine Situation wie oben bei den ISINs zu vermeiden, bei denen alles richtig ist, das Ergebnis aber dennoch falsch ist ?


Freundliche Grüsse, Ralf

 

[antaris]

Hallo Ralf,

wie gelingt es Dir, eine Situation wie oben bei den ISINs zu vermeiden, bei denen alles richtig ist, das Ergebnis aber dennoch falsch ist ?

was meinst du? Es wird doch von der richtigen Seite gemacht. Der Weg dahin ist vielleicht unnötig lang aber das Ziel wurde doch erreicht.

 

[TomS]

Im gesamten Repo liegen 270 Lean-Module, mit insgesamt 33 472 Zeilen. Es gibt dort 1 420 Docstrings (/--), 366 Modul-Dokblöcke (/-!), 690 Zeilenkommentare und 54 weitere Blockkommentare. Da ist allein die Überprüfung schon ziemlich aufwändig.
Die AI selbst muss irgendwas interpretieren, wenn ein Kommentar erstellt wird und das wird wahrscheinlich sehr schwer werden.

Programs are meant to be read by humans and only incidentally for computers to execute.
(Donald Knuth)

Sorry, das ist für praktische Arbeit völlig untauglich.

Wenn ich Code, den ich selbst geschrieben habe, um meine Intention und komplexe Zusammenhänge auszudrücken, nicht mehr verstehe und dies dadurch kompensieren muss, dass ich Code kommentiere, was jedoch alsbald inkonsistent wird, sobald ich den Code ändere (ändern muss), dann ist mir nicht mehr zu helfen. Der Code muss ohne weiter Kommentare erklären, was im Code passiert; die Dokumentation ggf. warum.

In diesem Sinne ...

Don’t comment bad code—rewrite it.
Brian Kernigham

 

[TomS]

import Mathlib.Data.Matrix.Basic
import Mathlib.LinearAlgebra.Matrix.Hermitian
import Mathlib.Analysis.InnerProductSpace.Basic

open Complex
open Matrix

variable {n : Type} [Fintype n] [DecidableEq n]

theorem eigenvalue_real_of_hermitian
  (A : Matrix n n ℂ)
  (hA : A.IsHermitian)
  (λ : ℂ)
  (v : n → ℂ)
  (hv : v ≠ 0)
  (hAv : A.mulVec v = λ • v) :
  λ ∈ ℝ := by

  have h1 : ⟪v, A.mulVec v⟫ = λ * ⟪v, v⟫ := by
    simp [hAv]

  have h2 : ⟪v, A.mulVec v⟫ = ⟪A.mulVec v, v⟫ := by
    simpa using hA.inner_mulVec_eq (v := v) (w := v)

  have h3 : ⟪A.mulVec v, v⟫ = conj λ * ⟪v, v⟫ := by
    simp [hAv]

  have hλ : λ * ⟪v, v⟫ = conj λ * ⟪v, v⟫ := by
    simpa [h1, h2, h3]

  have hvv : ⟪v, v⟫ ≠ 0 := by
    exact inner_self_ne_zero.mpr hv

  have : λ = conj λ := by
    exact mul_right_cancel₀ hvv hλ

  exact Complex.eq_real_of_conj_eq this

Etwas gewöhnungsbedürftig, aber handhabbar.

 

[ralfkannenberg]

dieser code generiert oder prüft keine ISIN-codes. Das ist ein fehlerfreier -> kompilierter lean-Beweis mit dem Ziel "* The theorem proves that the computed check digit always verifies."

was meinst du? Es wird doch von der richtigen Seite gemacht. Der Weg dahin ist vielleicht unnötig lang aber das Ziel wurde doch erreicht.

Hallo Antaris,

ich bin verwirrt, aber ja, in Deinen Ausführungen habe ich nun auch das gefunden:

Antwort claude:

Das ist eine berechtigte Beobachtung, aber der Code macht es tatsächlich bereits korrekt – und zwar von links nach rechts.

(...)

Der Unterschied zum "klassischen" Luhn: Beim Kreditkarten-Luhn zählt man von rechts nach links, wobei die Prüfziffer (ganz rechts) nicht verdoppelt wird und die zweite von rechts schon. Bei der ISIN wird dagegen von links nach rechts gezählt – aber welche Positionen verdoppelt werden, ist am Ende dasselbe, weil es nur darauf ankommt, welche Ziffern auf geraden bzw. ungeraden Positionen liegen.

Irgendwie möchte ich mich nicht bei einem Code, der in 3 Zeilen implementierbar ist, durch Kommentare durchlesen müssen mit dem Risiko, das Wesentliche zu überlesen, zumal Du zunächst ja selber geschrieben hattest, dass keine ISIN-codes überprüft werden. Offenbar geschieht das aber doch - und zudem noch korrekt


Freundliche Grüsse, Ralf

 

[antaris]

Wenn ich Code, den ich selbst geschrieben habe, um meine Intention und komplexe Zusammenhänge auszudrücken, nicht mehr verstehe und dies dadurch kompensieren muss, dass ich Code kommentiere, was jedoch alsbald inkonsistent wird, sobald ich den Code ändere (ändern muss), dann ist mir nicht mehr zu helfen. Der Code muss ohne weiter Kommentare erklären, was im Code passiert; die Dokumentation ggf. warum.

Ich habe tatsächlich schon daran gedacht die Kommentare einfach alle rauszulöschen. Kommentiert wird ja eigentlich auch eher, wenn fertig ist.
Ich denke aber Kommentare sind nicht nur für ein selber da, sondern für das Verständnis anderer. Ich bin ja nicht der Programmierer gewesen, nur der Richtungsgeber.

In diesem Sinne ...

Don’t comment bad code—rewrite it.
Brian Kernigham

Das muss ich sowieso aber bis dahin hätte ich ziemlich viele Fragen,,,
Es existiert eine relativ große Lean-Community mit Forum usw.. In den Docs zu lean wird aber schon auch auf kommenteiren hingewiesen. Ich werde einen minimalen Ansatz wählen bzw. das wird schon umgebaut. Kommentar Änderungsplan und Regelwerk angelehnt an die Dokumentation von lean/mathlib: https://chatgpt.com/canvas/shared/69c6b58a42208191ba33e6ee0938effd

 

[antaris]

Etwas gewöhnungsbedürftig, aber handhabbar.

Hast du das selber geschrieben und auch kompiliert?
Ja ich sehe was du meinst, denn anhand der Variablennamen sieht man schon, wo man ist. Das problem ist, das z.B. UTF-8 und auch nicht alle Sonderzeichen erlaubt sind. Das begrenzt die Freiheit in der Namensgebung. Dein code kompiliert bei mir nicht, wegen den Variablen.


Ich habe das als isHermitian.lean in mein Repo gelegt und den build gestartet.

PS G:\leanwork\REAL-OQS> lake build .\REALOQS\isHermitian.lean

✖ [2216/2216] Building REALOQS.isHermitian

trace: .> LEAN_PATH=G:\leanwork\REAL-OQS\.lake\packages\Cli\.lake\build\lib\lean;G:\leanwork\REAL-OQS\.lake\packages\batteries\.lake\build\lib\lean;G:\leanwork\REAL-OQS\.lake\packages\Qq\.lake\build\lib\lean;G:\leanwork\REAL-OQS\.lake\packages\aesop\.lake\build\lib\lean;G:\leanwork\REAL-OQS\.lake\packages\proofwidgets\.lake\build\lib\lean;G:\leanwork\REAL-OQS\.lake\packages\importGraph\.lake\build\lib\lean;G:\leanwork\REAL-OQS\.lake\packages\LeanSearchClient\.lake\build\lib\lean;G:\leanwork\REAL-OQS\.lake\packages\plausible\.lake\build\lib\lean;G:\leanwork\REAL-OQS\.lake\packages\mathlib\.lake\build\lib\lean;G:\leanwork\REAL-OQS\.lake\build\lib\lean c:\Users\Jan\.elan\toolchains\leanprover--lean4---v4.24.0\bin\lean.exe G:\leanwork\REAL-OQS\REALOQS\isHermitian.lean -o G:\leanwork\REAL-OQS\.lake\build\lib\lean\REALOQS\isHermitian.olean -i G:\leanwork\REAL-OQS\.lake\build\lib\lean\REALOQS\isHermitian.ilean -c G:\leanwork\REAL-OQS\.lake\build\ir\REALOQS\isHermitian.c --setup G:\leanwork\REAL-OQS\.lake\build\ir\REALOQS\isHermitian.setup.json --json

error: REALOQS/isHermitian.lean:13:3: unexpected token 'λ'; expected '_' or identifier

warning: REALOQS/isHermitian.lean:37:39: '' starts on column 39, but all commands should start at the beginning of the line.


Note: This linter can be disabled with `set_option linter.style.commandStart false`

error: Lean exited with code 1

Some required targets logged failures:

- REALOQS.isHermitian

error: build failed