Eine ontologische Re-Interpretation offener Quantensysteme?!

[antaris]

Dein code kompiliert bei mir nicht, wegen den Variablen.

λ ist eine reservierte Variable, die ich im code einfach mit u ersetzt habe. Dann läuft der build weiter, stoppt aber im Beweis. Das ist genau was ich meine, dass lean nicht exakt wie normale Mathematik funktioniert. Der Aufbau der Beweise ist anders und es müssen exakt die mathlib-API Namen verwendet werden.

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:19:12: expected token
error: REALOQS/isHermitian.lean:17:2: failed to synthesize

  Membership ℂ Type

Hint: Additional diagnostic information may be available using the `set_option diagnostics true` command.
error: REALOQS/isHermitian.lean:19:7: Missing cases:
error: REALOQS/isHermitian.lean:17:11: unsolved goals
n : Type
inst✝¹ : Fintype n
inst✝ : DecidableEq n
A : Matrix n n ℂ
hA : A.IsHermitian
u : ℂ
v : n → ℂ
hv : v ≠ 0
hAv : A *ᵥ v = u • v
h1 : sorry
⊢ sorry

 

[antaris]

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

Hier die Antwort von claude zum Hermitizitätsbeweis im Repo.



TomS' Argument in #250 ist mathematisch korrekt — für eine allgemeine Komplexifizierung. Er sagt: Wenn H = L₁ + iL₂ mit zwei reellen Matrizen L₁, L₂, dann braucht man für H* = H die Bedingungen L₁ᵀ = L₁ und L₂ᵀ = −L₂. Die Symmetrie L₁ᵀ = L₁ allein reicht nicht, wenn L₂ beliebig ist. Das ist vollkommen richtig.



Aber der Code macht keine allgemeine Komplexifizierung. Schau dir die Definition an:



lean

def fullHamiltonian (L : Matrix Ω Ω ℝ) : Mat Ω :=
fun i j => (L i j : ℂ)

Das nimmt eine reelle Matrix L und setzt jeden Eintrag als komplexe Zahl ein — mit Imaginärteil Null. In TomS' Notation: L₁ = L und L₂ = 0. Es gibt kein iL₂.

Für L₂ = 0 ist TomS' zweite Bedingung L₂ᵀ = −L₂ trivial erfüllt (0ᵀ = 0 = −0). Also reicht L₁ᵀ = L₁, also Lᵀ = L, tatsächlich aus.


Das Theorem im Code ist also korrekt. Es sagt nicht „für eine allgemeine Komplexifizierung", sondern: „Wenn H durch fun i j => (L i j : ℂ) definiert ist" — also rein reelle Einträge — „und Lᵀ = L, dann H* = H." Lean verifiziert das ohne Fehler.

Das Problem war und bleibt das Wort „Komplexifizierung". TomS liest den Satz „Komplexifizierung + Lᵀ = L → hermitesch" und sagt zu Recht: Das stimmt im allgemeinen Fall nicht. Und er hat recht — im allgemeinen Fall V(ℂ) = V ⊕ iV stimmt es nicht. Aber der Code macht nicht den allgemeinen Fall. Er macht den Spezialfall L₂ = 0.

Das Wort „Komplexifizierung" war falsch — korrekt ist „Einbettung reeller Einträge in ℂ".

 

[ralfkannenberg]

Das nimmt eine reelle Matrix L und setzt jeden Eintrag als komplexe Zahl ein — mit Imaginärteil Null.

Hallo Antaris,

da habe ich etwas nicht verstanden: mit dieser "Methode" kann man zeigen, dass jede komplexe Zahl reell-wertig ist.

Aber der Code macht nicht den allgemeinen Fall. Er macht den Spezialfall L₂ = 0.

Das Wort „Komplexifizierung" war falsch — korrekt ist „Einbettung reeller Einträge in ℂ".

Warum diese Einschränkung ?


Freundliche Grüsse, Ralf

 

[antaris]

Hallo Ralf,

da habe ich etwas nicht verstanden: mit dieser "Methode" kann man zeigen, dass jede komplexe Zahl reell-wertig ist.

Der Code startet mit einer reellen Matrix L : Matrix Ω Ω ℝ und bettet sie nach ℂ ein. Die Einträge sind reell, weil L reell ist, nicht weil die Einbettung irgendetwas reell macht. Man kann mit dieser Methode nicht zeigen, dass 3+4i reell ist, denn 3+4i ist kein Element von ℝ und kann gar nicht als Input dienen. Die Typsignatur L : Matrix Ω Ω ℝ erzwingt, dass nur reelle Matrizen hineingehen.

Warum diese Einschränkung ?

Weil L aus Pillar A kommt und dort ein reeller Operator ist -> der DtN-Randoperator des ToC bzw. Graph-Laplacians. Graph-Laplacians sind reell und symmetrisch. Es gibt keinen physikalischen Grund, einen Imaginärteil hinzuzufügen.

 

[TomS]

Hast du das selber geschrieben und auch kompiliert?

Ich habe den Beweis bei ChatGPT hochgeladen und mir den Code generieren lassen. Nur aus Neugierde.

 

[antaris]

Ich habe den Beweis bei ChatGPT hochgeladen und mir den Code generieren lassen. Nur aus Neugierde.

ChatGPT hat das dann nach "besten Wissen und Gewissen" gemacht aber eben nicht explizit gemäß den mathlib docs. Selbst wenn letzteres verlangt wird, ist es eher selten, dass der code beim ersten Versuch kompiliert.

 

[TomS]

Das war auch nicht das Ziel der Übung. Es ging lediglich darum, wie Lean prinzipiell arbeitet, und wie ein bekannter Beweis in Lean repräsentiert wird.

So wie ich das sehe, muss ich wissen, was ich beweisen will, und den Beweis (kleinteilig strukturier) vorgeben; mittels Lean kann ich das prüfen lassen. Damit ist Lean relevant, wenn Beweise extrem unübersichtlich wird.

 

[antaris]

Damit ist Lean relevant, wenn Beweise extrem unübersichtlich wird.

Das Lemma quadForm_ext_eq_quadForm_blockII in REALOQS/PillarA/Ideal/TreeOfCliques/DtNStabilizedGate.lean ist mit 161 Zeilen das längste.

lemma quadForm_ext_eq_quadForm_blockII
    (k : Nat) (Lk : Matrix (Vertex b k) (Vertex b k) ℝ)
    (x : (sSplit (b := b) k).I → ℝ) :
    let g : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I) → ℝ := fun s =>
      match s with
      | Sum.inl _ => 0
      | Sum.inr i => x i
    let f : Vertex b k → ℝ := fun v => g ((sSplit (b := b) k).e v)
    PillarA.LayerA.quadForm Lk f =
      PillarA.LayerA.quadForm ((sSplit (b := b) k).blockII Lk) x := by
  classical
  intro g f
  change (∑ v : Vertex b k, f v * (∑ w : Vertex b k, Lk v w * f w))
      = (∑ i : (sSplit (b := b) k).I,
          x i * (∑ j : (sSplit (b := b) k).I, ((sSplit (b := b) k).blockII Lk) i j * x j))

  have houter :
      (∑ v : Vertex b k, f v * (∑ w : Vertex b k, Lk v w * f w))
        =
      (∑ s : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I),
        f (((sSplit (b := b) k).e).symm s) *
          (∑ w : Vertex b k, Lk (((sSplit (b := b) k).e).symm s) w * f w)) := by
    simpa using
      (Fintype.sum_equiv (sSplit (b := b) k).e
        (fun v : Vertex b k => f v * (∑ w : Vertex b k, Lk v w * f w))
        (fun s : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I) =>
          f (((sSplit (b := b) k).e).symm s) *
            (∑ w : Vertex b k,
              Lk (((sSplit (b := b) k).e).symm s) w * f w))
        (by intro v; simp))

  have hinner :
      ∀ s : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I),
        (∑ w : Vertex b k, Lk (((sSplit (b := b) k).e).symm s) w * f w)
          =
        (∑ t : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I),
          Lk (((sSplit (b := b) k).e).symm s) (((sSplit (b := b) k).e).symm t) *
            f (((sSplit (b := b) k).e).symm t))
        := by
    intro s
    simpa using
      (Fintype.sum_equiv (sSplit (b := b) k).e
        (fun w : Vertex b k => Lk (((sSplit (b := b) k).e).symm s) w * f w)
        (fun t : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I) =>
          Lk (((sSplit (b := b) k).e).symm s) (((sSplit (b := b) k).e).symm t) *
            f (((sSplit (b := b) k).e).symm t))
        (by intro w; simp))

  have hf :
      ∀ s : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I),
        f (((sSplit (b := b) k).e).symm s) = g s := by
    intro s
    simp [f]

  have hLHS :
      (∑ v : Vertex b k, f v * (∑ w : Vertex b k, Lk v w * f w))
        =
      (∑ s : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I),
        g s * (∑ t : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I),
          Lk (((sSplit (b := b) k).e).symm s) (((sSplit (b := b) k).e).symm t) * g t)) := by
    calc
      (∑ v : Vertex b k, f v * (∑ w : Vertex b k, Lk v w * f w))
          =
        (∑ s : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I),
          f (((sSplit (b := b) k).e).symm s) *
            (∑ w : Vertex b k, Lk (((sSplit (b := b) k).e).symm s) w * f w)) := houter
      _ =
        (∑ s : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I),
          f (((sSplit (b := b) k).e).symm s) *
            (∑ t : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I),
              Lk (((sSplit (b := b) k).e).symm s) (((sSplit (b := b) k).e).symm t) *
                f (((sSplit (b := b) k).e).symm t)))
        := by
        refine Fintype.sum_congr
          (fun s : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I) =>
            f (((sSplit (b := b) k).e).symm s) *
              (∑ w : Vertex b k,
                Lk (((sSplit (b := b) k).e).symm s) w * f w))
          (fun s : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I) =>
            f (((sSplit (b := b) k).e).symm s) *
              (∑ t : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I),
                Lk (((sSplit (b := b) k).e).symm s) (((sSplit (b := b) k).e).symm t) *
                  f (((sSplit (b := b) k).e).symm t)))
          (by
            intro s
            exact congrArg (fun z => f (((sSplit (b := b) k).e).symm s) * z) (hinner s))
      _ = _ := by
        simp [hf]

  have hSplitOuter :
      (∑ s : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I),
        g s * (∑ t : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I),
          Lk (((sSplit (b := b) k).e).symm s) (((sSplit (b := b) k).e).symm t) * g t))
        =
      (∑ bb : (sSplit (b := b) k).B,
        g (Sum.inl bb) * (∑ t : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I),
          Lk (((sSplit (b := b) k).e).symm (Sum.inl bb)) (((sSplit (b := b) k).e).symm t) * g t))
      +
      (∑ ii : (sSplit (b := b) k).I,
        g (Sum.inr ii) * (∑ t : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I),
          Lk (((sSplit (b := b) k).e).symm (Sum.inr ii))
              (((sSplit (b := b) k).e).symm t) * g t))
        := by
    simp [Fintype.sum_sum_type]

  have hInnerI :
      ∀ ii : (sSplit (b := b) k).I,
        (∑ t : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I),
          Lk (((sSplit (b := b) k).e).symm (Sum.inr ii)) (((sSplit (b := b) k).e).symm t) * g t)
          =
        (∑ jj : (sSplit (b := b) k).I,
          Lk (((sSplit (b := b) k).e).symm (Sum.inr ii))
              (((sSplit (b := b) k).e).symm (Sum.inr jj)) * x jj)
        := by
    intro ii
    calc
      (∑ t : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I),
        Lk (((sSplit (b := b) k).e).symm (Sum.inr ii)) (((sSplit (b := b) k).e).symm t) * g t)
          =
        (∑ bb : (sSplit (b := b) k).B,
          Lk (((sSplit (b := b) k).e).symm (Sum.inr ii))
              (((sSplit (b := b) k).e).symm (Sum.inl bb)) * g (Sum.inl bb))
        +
        (∑ jj : (sSplit (b := b) k).I,
          Lk (((sSplit (b := b) k).e).symm (Sum.inr ii))
              (((sSplit (b := b) k).e).symm (Sum.inr jj)) * g (Sum.inr jj))
        := by
        simp [Fintype.sum_sum_type]
      _ =
        (∑ jj : (sSplit (b := b) k).I,
          Lk (((sSplit (b := b) k).e).symm (Sum.inr ii))
              (((sSplit (b := b) k).e).symm (Sum.inr jj)) * x jj)
        := by
        simp [g]

  calc
    (∑ v : Vertex b k, f v * (∑ w : Vertex b k, Lk v w * f w))
        =
      (∑ s : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I),
        g s * (∑ t : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I),
          Lk (((sSplit (b := b) k).e).symm s) (((sSplit (b := b) k).e).symm t) * g t)) := hLHS
    _ =
      (∑ bb : (sSplit (b := b) k).B,
        g (Sum.inl bb) * (∑ t : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I),
          Lk (((sSplit (b := b) k).e).symm (Sum.inl bb)) (((sSplit (b := b) k).e).symm t) * g t))
      +
      (∑ ii : (sSplit (b := b) k).I,
        g (Sum.inr ii) * (∑ t : Sum ((sSplit (b := b) k).B) ((sSplit (b := b) k).I),
          Lk (((sSplit (b := b) k).e).symm (Sum.inr ii))
              (((sSplit (b := b) k).e).symm t) * g t)) := hSplitOuter
    _ =
      (∑ ii : (sSplit (b := b) k).I,
        x ii * (∑ jj : (sSplit (b := b) k).I,
          Lk (((sSplit (b := b) k).e).symm (Sum.inr ii))
              (((sSplit (b := b) k).e).symm (Sum.inr jj)) * x jj))
        := by
        simp [g, hInnerI]
    _ =
      (∑ ii : (sSplit (b := b) k).I,
        x ii * (∑ jj : (sSplit (b := b) k).I, ((sSplit (b := b) k).blockII Lk) ii jj * x jj)) := by
      simp [PillarA.OQS.Split.blockII, PillarA.OQS.Split.reindex, Matrix.reindex]

 

[antaris]

Am komplexesten ist das Theorem sum_all_real1_pos in REALOQS/PillarA/Physics/Instances/TreeOfCliquesBreakWitness.lean:647–794. Es import einige andere Module und nutzt diese im Beweis. Er erstreckt sich damit nicht nur über die Zeilen im eigentlichen Modul, sondern darüber hinaus auch über andere Module. Solche verzweigten Beweise kommen auch noch in etwas kleineren Größenordungen an anderen Stellen vor.

theorem sum_all_real1_pos
    (p : _root_.PillarA.LayerA.Policy b) (hb : 0 < b) :
    0 <
      (∑ x : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
        ∑ y : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
          (_root_.PillarA.Ideal.TreeOfCliques.DtNStabilized.dtn_stabilized
              (b := b) (p := p) 1) x y) := by
  classical
  let L1 := _root_.PillarA.Ideal.TreeOfCliques.DtNStabilized.L (b := b) 1
  let s1 := _root_.PillarA.Ideal.TreeOfCliques.DtNStabilized.s (b := b) 1
  let δ : ℝ :=
    _root_.PillarA.OQS.Split.DtNStabilized.deltaNum p
      (_root_.PillarA.OQS.Split.DtNStabilized.symm (s1.blockII L1))
  let Schur :
      Matrix (_root_.PillarA.Ideal.TreeOfCliques.Boundary b 1)
        (_root_.PillarA.Ideal.TreeOfCliques.Boundary b 1) ℝ :=
    s1.blockBI L1 *
        (_root_.PillarA.Ideal.TreeOfCliques.DtNStabilized.LII_stab p 1)⁻¹ *
      s1.blockIB L1

  have hbR : 0 < (b : ℝ) := by exact_mod_cast hb
  have hδpos : 0 < δ := by
    simpa [δ] using (delta_pos_k1 (b := b) (p := p))
  have hbδpos : 0 < (b : ℝ) + δ := add_pos hbR hδpos
  have hbδne : (b : ℝ) + δ ≠ 0 := ne_of_gt hbδpos

  have hSchurEntry :
      ∀ x y : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
        Schur x y = ((b : ℝ) + δ)⁻¹ := by
    intro x y
    simpa [Schur, L1, s1, δ] using
      (schur_entry_const_k1 (b := b) (p := p) x y)

  have hcells :
      (_root_.PillarA.Ideal.cellsAtLevel b 1).card = b := by
    simpa using (_root_.PillarA.Ideal.card_cellsAtLevel b 1)

  have hcellsR :
      (( _root_.PillarA.Ideal.cellsAtLevel b 1).card : ℝ) = (b : ℝ) := by
    exact_mod_cast hcells

  have hsumSchur :
      (∑ x : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
        ∑ y : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
          Schur x y)
        = (b : ℝ) * (b : ℝ) * ((b : ℝ) + δ)⁻¹ := by
    have h' :
        (∑ x : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
          ∑ y : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
            Schur x y)
          =
          (( _root_.PillarA.Ideal.cellsAtLevel b 1).card : ℝ) *
            ((( _root_.PillarA.Ideal.cellsAtLevel b 1).card : ℝ) *
              ((b : ℝ) + δ)⁻¹) := by
        simp [hSchurEntry, Finset.sum_const, nsmul_eq_mul]
    have h'' :
        (∑ x : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
          ∑ y : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
            Schur x y)
          = (b : ℝ) * ((b : ℝ) * ((b : ℝ) + δ)⁻¹) := by
      simpa [hcellsR] using h'
    simpa [mul_assoc] using h''

  have hsumDtN :
      (∑ x : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
        ∑ y : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
          (_root_.PillarA.Ideal.TreeOfCliques.DtNStabilized.dtn_stabilized
              (b := b) (p := p) 1) x y)
        =
      (∑ x : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
        ∑ y : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
          s1.blockBB L1 x y) -
        (∑ x : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
          ∑ y : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
            Schur x y) := by
    simp [ _root_.PillarA.Ideal.TreeOfCliques.DtNStabilized.dtn_stabilized,
      _root_.PillarA.Ideal.TreeOfCliques.DtNStabilized.dtn_stabilized_of_det,
      _root_.PillarA.OQS.Split.DtNStabilized.dtn_stabilized_of_det,
      _root_.PillarA.OQS.Split.DtNStabilized.DtN_stabilized_of,
      _root_.PillarA.OQS.Split.DtNStabilized.interiorInvStabilized_of_det,
      _root_.PillarA.OQS.Split.DtNStabilized.LII_stabilized,
      _root_.PillarA.LayerA.DtN,
      Schur, L1, s1,
      Matrix.sub_apply, Finset.sum_sub_distrib]

  have hsumLBB :
      (∑ x : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
        ∑ y : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
          s1.blockBB L1 x y) = (b : ℝ) := by
    simpa [L1, s1] using (sum_all_LBB_eq_b (b := b))

  have hsumSchur_attach :
      (∑ x ∈ (_root_.PillarA.Ideal.cellsAtLevel b 1).attach,
        ∑ y ∈ (_root_.PillarA.Ideal.cellsAtLevel b 1).attach,
          Schur x y)
        = (b : ℝ) * (b : ℝ) * ((b : ℝ) + δ)⁻¹ := by
    simpa using hsumSchur

  have hsumLBB_attach :
      (∑ x ∈ (_root_.PillarA.Ideal.cellsAtLevel b 1).attach,
        ∑ y ∈ (_root_.PillarA.Ideal.cellsAtLevel b 1).attach,
          s1.blockBB L1 x y) = (b : ℝ) := by
    simpa using hsumLBB

  have hsumEq :
      (∑ x : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
        ∑ y : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
          (_root_.PillarA.Ideal.TreeOfCliques.DtNStabilized.dtn_stabilized
              (b := b) (p := p) 1) x y)
        = (b : ℝ) - (b : ℝ) * (b : ℝ) * ((b : ℝ) + δ)⁻¹ := by
    calc
      (∑ x : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
        ∑ y : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
          (_root_.PillarA.Ideal.TreeOfCliques.DtNStabilized.dtn_stabilized
              (b := b) (p := p) 1) x y)
          =
        (∑ x : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
          ∑ y : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
            s1.blockBB L1 x y) -
          (∑ x : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
            ∑ y : _root_.PillarA.Ideal.TreeOfCliques.Boundary b 1,
              Schur x y) := by
          exact hsumDtN
      _ = (b : ℝ) - (b : ℝ) * (b : ℝ) * ((b : ℝ) + δ)⁻¹ := by
          simp [hsumLBB_attach, hsumSchur_attach]

  have hsumEq_attach :
      (∑ x ∈ (_root_.PillarA.Ideal.cellsAtLevel b 1).attach,
        ∑ y ∈ (_root_.PillarA.Ideal.cellsAtLevel b 1).attach,
          (_root_.PillarA.Ideal.TreeOfCliques.DtNStabilized.dtn_stabilized
              (b := b) (p := p) 1) x y)
        = (b : ℝ) - (b : ℝ) * (b : ℝ) * ((b : ℝ) + δ)⁻¹ := by
    simpa using hsumEq

  have hrewrite :
      (b : ℝ) - (b : ℝ) * (b : ℝ) * ((b : ℝ) + δ)⁻¹
        = (b : ℝ) * δ * ((b : ℝ) + δ)⁻¹ := by
    field_simp [hbδne]
    ring_nf

  have hinvpos : 0 < ((b : ℝ) + δ)⁻¹ := inv_pos.2 hbδpos
  have hbδ : 0 < (b : ℝ) * δ := mul_pos hbR hδpos
  have hpos : 0 < (b : ℝ) * δ * ((b : ℝ) + δ)⁻¹ := by
    have : 0 < ((b : ℝ) * δ) * ((b : ℝ) + δ)⁻¹ := mul_pos hbδ hinvpos
    simpa [mul_assoc] using this

  simpa [hsumEq_attach, hrewrite] using hpos

 

[antaris]

Bezüglich den Kommentaren habe ich mich, nach ein paar Tests mit verscheidenen AI's , dazu entschieden sämtliche Kommentare aus den Dateien zu entfernen.

Ich habe einige von Kommentare befreite Theoreme von AI's erklären lassen und die Aussagen/Antworten waren zwar unterschiedlich strukturiert aber inhaltlich identisch. Dazu ist jedes Zeichen weniger in den Modulen, freundlicher für die Maschinen zu lesen. Kommentare im code sind dahingehend eher hinderlich. Für mich selbst benötige ich keine Kommentare. Ich habe zwar lange nicht die mathematischen Details verstanden aber der Projektaufbau und die Intention hinter den Modulen kommt ja aus meinen Kopf. Insofern kenne ich mich innerhalb des Repos genügend aus um zu wissen was wo passiert. Auf dieser Basis werde ich nun nochmal die Pillar, den strikten Pfad und den gesamten Stand mittels .tex dokumentieren. Ich weiß ja nun auch wie Beweise zu dokumentieren sind und lasse das konsequent umsetzen.

Da es sich um ein Proof of Concept handelt, ist der Stand jetzt sozusagen final, obwohl bei weitem nicht abgeschlossen. Das bedeutet die Dokumentation wäre dann auch auf den jetzigen kommentarlosen code-Stand fixiert.

 

[Bernhard]

Das war auch nicht das Ziel der Übung. Es ging lediglich darum, wie Lean prinzipiell arbeitet, und wie ein bekannter Beweis in Lean repräsentiert wird.

Ist Lean eine Software? Gibt es Links, die erklären, was Lean macht und von wem es geschrieben wurde?

 

[antaris]

Ist Lean eine Software?

Lean ist eine formale Programmiersprache und Beweisassistent in einem, sowie open source lizensiert.

Gibt es Links, die erklären, was Lean macht

https://lean-lang.org/
https://leanprover-community.github.io/
https://en.wikipedia.org/wiki/Lean_(proof_assistant)

und von wem es geschrieben wurde?

https://en.wikipedia.org/wiki/Leonardo_de_Moura

 

[Bernhard]

Da es sich um ein Proof of Concept handelt, ist der Stand jetzt sozusagen final, obwohl bei weitem nicht abgeschlossen.

Ein interessantes Thema darüber, was alles passiert, wenn man die Kontrolle an eine AI abgibt

 

[antaris]

Ein interessantes Thema darüber, was alles passiert, wenn man die Kontrolle an eine AI abgibt

Inwiefern? Ein Proof of Concept soll zeigen, dass der Formalismus innerhalb des lean-codes grundsätzlich funktioniert und nicht die ganze Physik auf einmal reproduzieren. Ich kann klar benennen wo die offenen Baustellen liegen, was im strikten Pfad vom ToC bis zu den Endobjekten wirklich tragbar ist und woran weitergearbeitet werden muss.

 

[Bernhard]

https://lean-lang.org/
https://leanprover-community.github.io/
https://en.wikipedia.org/wiki/Lean_(proof_assistant)

https://en.wikipedia.org/wiki/Leonardo_de_Moura

OK. Danke für die Links. Das kann man sich dann mal genauer ansehen.

Man könnte eventuell ein eigenes Thema über Beweisassistenten aufmachen und dort darüber diskutieren, welche Qualitätskriterien es bei diesen geben könnte oder sollte. Ich bin diesbezüglich ziemlich skeptisch eingestellt.

 

[antaris]

Ich bin diesbezüglich ziemlich skeptisch eingestellt.

Was vollkommen in Ordnung ist.
Man kann natürlich auch mal schauen, welche Profis damit schon gearbeitet und was genau die so alles gemacht haben...

 

[TomS]

@antaris – Da zeigt sich das wesentliche Problem: Man muss Lean sehr gut beherrschen, um Voraussetzung und Theorem lesen und verstehen zu können. Das ist so ein bisschen wie Mathe und Python. Und sehe ich bzgl. der Lesbarkeit des Codes tatsächlich deutlichen Verbesserungsbedarf.

Allerdings kommt es natürlich sehr stark auf den Anwendungsfall an. Niemand wird Beweise, zu denen ein hohes Maß an Kreativität erforderlich ist, bei denen es ständig vorwärts und rückwärts geht, Ansätze verworfen werden … in Lean packen. Man wird stattdessen Teile von Beweisen, in denen z.B. 1000 Spezialfälle zu untersuchen sind, diese automatisiert auf Lean-Code abbilden.

 

[TomS]

Ich bin diesbezüglich ziemlich skeptisch eingestellt.

Lean (Beweisassistent) – Wikipedia

de.wikipedia.org

Der Mathematiker Peter Scholze erhielt 2018 die Fields-Medaille für seine Arbeit über perfektoide Räume. Kevin Buzzard formulierte diese Theorie in Lean und als Scholze 2019 einen Beweis für einen neuen Satz vorlegte, wurde dieser in Lean formuliert und als „Liquid Tensor Project“ abgeschlossen, mit dem Ergebnis, dass der Beweis aus Sicht von Lean korrekt ist.

 

[antaris]

Da zeigt sich das wesentliche Problem: Man muss Lean sehr gut beherrschen, um Voraussetzung und Theorem lesen und verstehen zu können. Das ist so ein bisschen wie Mathe und Python.

Das stimmt. Für ein "menschliches" Review ist das unabdingbar.

Und sehe ich bzgl. der Lesbarkeit des Codes tatsächlich deutlichen Verbesserungsbedarf.

Das ist ein Punkt, den ich vorher sogar bewusst unterdrückt hatte. Die AI sollte sich auf den code konzentrieren. Jede zusätzliche "Aufgabe" hätte mehr Fehler hineingetragen. Insgesamt habe ich die Woche gelernt, wie sowas generell zu strukturieren ist und worauf der Fokus gelegt sein sollte. Das hilft mir in jedem Fall weiter.

Allerdings kommt es natürlich sehr stark auf den Anwendungsfall an. Niemand wird Beweise, zu denen ein hohes Maß an Kreativität erforderlich ist, bei denen es ständig vorwärts und rückwärts geht, Ansätze verworfen werden … in Lean packen.

Warum nicht? Lean erfodert entweder klare benennungen von Lücken im Modell, wie z.B. mit konkreten axiom oder sorry. Ansonsten muss der Formalismus lückenlos programmiert werden. Es können keinen Annahmen vorausgesetzt werden, die man so wissen muss. Alles muss innerhalb das codes kompiliert werden.
Dazu kommt eben der Faktor der künstlichen Intelligenz. Ich habe das Repo mit ChatGPT nebenbei innerhalb von 2 Monate erstellt. Es ist etwas ganz anderes, wenn jahrelange Arbeit über den Haufen geworfen werden müsste oder insgesamt effektiv nur ein paar Tage. Wenn man erkennt, das man neu anfangen muss, dann weiß man ja warum, was bereits funktioniert/angepasst/übernommen und was verworfen werden kann. In einem neuen Schritt kann von vornherein auch mehr Wert auf die Lesbarkeit des codes gelegt werden, ohne wieder auf Kommentare zurückfallen zu müssen. Dazu zählt z.B., dass der AI nicht die freie Wahl von Variablennamen gelassen wird.

 

[TomS]

Warum nicht?

Weil Lean nicht den kreativen sondern den pedantischen Teil übernimmt. Und weil der kreative Teil am besten mit einem kreativen Sparringspartner funktioniert.

… kann von vornherein auch mehr Wert auf die Lesbarkeit des codes gelegt werden …

… was ja der Ausgangspunkt der Diskussion war. Und da ist die Sprache – vermutlich bewusst – schlicht nicht ausdrucksstark genug. Evtl. kann man das mit dem Schritt von TeX zu LaTeX vergleiche, d.h. man könnte eine Macro-Ebene über Lean legen.

Das sähe z.B. so aus:

⟪f, L, f⟫ = ⟪x, L_II, x⟫