Prove linear algebra by Aristotle

Stream: Machine Learning for Theorem Proving

[Nick_adfor]

I've tried to use Aristotle to prove a linear algebra theorem:

Aristotle failed to prove these (I may think the following one do not differ, but Aristotle may be able to prove them differently but all failed.):

import Mathlib

open Matrix

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

/- Aristotle failed to find a proof. -/
theorem Matrix.similar_to_standard_complex_form
    (A : Matrix n n ℝ) (hA : A ^ 2 + 1 = 0) :
    ∃ (m : ℕ) (hcard : Fintype.card n = 2 * m) (P : Matrix n n ℝ),
      IsUnit P ∧
      let e : n ≃ Fin (2 * m) := Fintype.equivFinOfCardEq hcard
      let B_block : Matrix (Fin 2) (Fin 2) ℝ := !![0, -1; 1, 0]
      let B_diag : Matrix (Fin 2 × Fin m) (Fin 2 × Fin m) ℝ := blockDiagonal (fun _ : Fin m => B_block)
      let equiv : (Fin 2 × Fin m) ≃ Fin (2 * m) := by exact finProdFinEquiv
      let B : Matrix (Fin (2 * m)) (Fin (2 * m)) ℝ := reindex equiv equiv B_diag
      P * A * P⁻¹ = reindex e.symm e.symm B := by
  sorry

/- Aristotle took a wrong turn (reason code: 9). Please try again. -/
theorem Matrix.similar_to_standard_complex_form'
    (A : Matrix n n ℝ) (hA : A ^ 2 + 1 = 0) :
    ∃ (m : ℕ) (hcard : Fintype.card n = 2 * m) (P : Matrix n n ℝ),
      IsUnit P ∧
      let e : n ≃ Fin (2 * m) := Fintype.equivFinOfCardEq hcard
      let equiv : (Fin 2 × Fin m) ≃ Fin (2 * m) := by exact finProdFinEquiv
      let B : Matrix (Fin (2 * m)) (Fin (2 * m)) ℝ :=
        reindex equiv equiv (blockDiagonal (fun _ : Fin m => !![0, -1; 1, 0]))
      P * A * P⁻¹ = reindex e.symm e.symm B := by
  sorry

/- Aristotle failed to find a proof. -/
theorem similar_to_block_form (A : Matrix n n ℝ) (h : A ^ 2 + (1 : Matrix n n ℝ) = 0) :
    ∃ (m : ℕ) (hcard : Fintype.card n = 2 * m)
       (P : Matrix n n ℝ) (Pinv : Matrix n n ℝ)
       (hinv : P * Pinv = 1) (hinv' : Pinv * P = 1),
    let e := Fintype.equivFinOfCardEq hcard
    let B : Matrix (Fin (2 * m)) (Fin (2 * m)) ℝ :=
      Matrix.of (fun i j =>
        if i.1 < m then
          if j.1 < m then (0 : ℝ)
          else if j.1 = i.1 + m then (-1 : ℝ) else 0
        else
          if j.1 < m then if i.1 = j.1 + m then (1 : ℝ) else 0
          else 0)
    P * A * Pinv = reindex e.symm e.symm B := by
  sorry

But there's a related one Aristotle can prove:

import Mathlib

open Matrix

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

theorem even_dim_of_A_sq_plus_id_eq_zero (A : Matrix n n ℝ) (h : A ^ 2 + (1 : Matrix n n ℝ) = 0) :
    ∃ m : ℕ, Fintype.card n = 2 * m := by
  -- Taking determinants on both sides of $A^2 + I = 0$, we get $\det(A^2) = \det(-I)$.
  have h_det : (Matrix.det A) ^ 2 = (-1 : ℝ) ^ (Fintype.card n) := by
    -- Since $A^2 = -I$, we can take the determinant of both sides to get $\det(A^2) = \det(-I)$.
    have h_det : Matrix.det (A^2) = Matrix.det (-1 : Matrix n n ℝ) := by
      rw [ eq_neg_of_add_eq_zero_left h ];
    aesop (config := {warnOnNonterminal := false});
    rw [ Matrix.det_neg ] ; norm_num;
  -- Since $(-1)^{Fintype.card n} = 1$, it follows that $Fintype.card n$ must be even.
  have h_even : (-1 : ℝ) ^ (Fintype.card n) = 1 := by
    by_cases h_even : Even ( Fintype.card n ) <;> simp_all +decide;
    nlinarith;
  rcases Nat.even_or_odd' ( Fintype.card n ) with ⟨ m, hm | hm ⟩ <;> norm_num [ hm ] at h_even ⊢

[Nick_adfor]

(deleted)

[Nick_adfor]

I may think it work this way in maths and write it as a note to inspire Aristotle, but nothing good happens.

-- Step 1: Show dimension is even using previous theorem
  -- From A² + I = 0, we know eigenvalues are ±i and come in conjugate pairs
  -- Therefore n must be even: n = 2m for some m ∈ ℕ

  -- Step 2: Define the equivalence between n and Fin(2m)

  -- Step 3: Construct the complex structure on ℝ^n
  -- A defines a complex structure: J = A satisfies J² = -I
  -- This makes ℝ^n into an m-dimensional complex vector space

  -- Step 4: Choose a complex basis and construct real basis
  -- Let {v₁, ..., vₘ} be a complex basis (over ℂ)
  -- Then {v₁, ..., vₘ, A v₁, ..., A vₘ} forms a real basis of ℝ^(2m)

  -- Step 5: Define the change-of-basis matrix P
  -- P is the matrix whose columns are the real basis vectors:
  -- [v₁, ..., vₘ, A v₁, ..., A vₘ]
  -- This P is invertible since it's a basis change

  -- Step 6: Compute P⁻¹AP in the new basis
  -- For 1 ≤ j ≤ m: A(v_j) = A v_j = (m+j)-th basis vector
  -- So (P⁻¹AP)(e_j) = e_{m+j} where e_j is j-th standard basis vector

  -- For m+1 ≤ j ≤ 2m: A(A v_{j-m}) = A² v_{j-m} = -v_{j-m}
  -- So (P⁻¹AP)(e_j) = -e_{j-m}

  -- Step 7: Verify this gives the block matrix B
  -- The matrix B has:
  -- - Zeros on diagonal blocks (i < m, j < m) and (i ≥ m, j ≥ m)
  -- - -1 in positions where j = i + m (upper right block)
  -- - 1 in positions where j = i - m (lower left block)

  -- Step 8: Construct P explicitly using the complex structure
  -- We need to find vectors v₁, ..., vₘ such that:
  -- {v₁, ..., vₘ, A v₁, ..., A vₘ} is linearly independent over ℝ

  -- Step 9: Use the minimal polynomial approach
  -- Since A² + I = 0, the minimal polynomial is x² + 1
  -- The rational canonical form gives the desired block structure

  -- Step 10: Alternatively, use the real Jordan form for complex eigenvalues
  -- Each conjugate pair ±i gives a 2×2 block [0 -1; 1 0]
  -- So A is similar to block diagonal of m copies of this 2×2 block

  -- This completes the construction showing A ∼ B via similarity P

  -- The actual Lean construction would involve:
  -- 1. Finding the invariant subspaces for the complex structure
  -- 2. Constructing the basis vectors explicitly
  -- 3. Building the change-of-basis matrix P
  -- 4. Verifying the similarity relation P * A * P⁻¹ = reindex e.symm e.symm B

[Kim Morrison]

Posting copies of attempts to use AI tools, without any questions or analysis, is off topic here (and even off topic in the machine learning channel).

[Notification Bot]

This topic was moved here from #general > Prove linear algebra by Aristotle by Kevin Buzzard.

[Kevin Buzzard]

Perhaps the people in this channel have some comments on use of the tool, or how to use it better etc? Otherwise I'm happy to delete completely.

[Nick_adfor]

Kim Morrison said:

Posting copies of attempts to use AI tools, without any questions or analysis, is off topic here (and even off topic in the machine learning channel).

Really no questions? The three theorems are the same in math but different in code. Different formulization will cause different tactic usable.

[Yury G. Kudryashov]

There were zero question marks in the original post and zero requests for help, only statements.

[Nick_adfor]

The truth is that I show the first question as "Is there one of these three theorem formulizations easier to prove than others"

[Nick_adfor]

But since I do not think it is necessary to check it one by one, I decide to choose the first theorem formulazation to prove first.

[Nick_adfor]

For the use Aristotle, I get a construction of the theorem proof (like have this; exact this, I call this to be the construction of the theorem proof just like the frame structure of a building.) and extract some of the lemmas (some have can be extracted as lemma and Aristotle might be able to solve them one by one, and it really helps.) But there's a left one, which I think might need a good construction proof (use Jordan) yet Aristotle failed, it might be Aristotle cannot write new definitions about Jordan and use the new definition.

-- Without n=2m can prove? If cannot, add it. In fact I've proved there exists n=2m.
lemma exists_similarity_transformation (A B : Matrix n n ℝ)
    (hA : A ^ 2 = -1) (hB : B ^ 2 = -1) : ∃ (P : Matrix n n ℝ), IsUnit P ∧ P * A * P⁻¹ = B := by
  sorry

So the problem now is how to use Jordan with the help of Aristotle (I may think that Aristotle cannot help to write the definition of Jordan decomposition.) to prove this. The math statement is

The original mathematical problem is:

Theorem: Let $A$ be an $n \times n$ real matrix such that $A^2 + I = 0$, where $I$ is the identity matrix. Prove that:

1. $n$ must be even, i.e., there exists $m \in \mathbb{N}$ such that $n = 2m$
2. $A$ is similar to the block diagonal matrix $B = \begin{pmatrix} 0 & -I_m \\ I_m & 0 \end{pmatrix}$, where $I_m$ is the $m \times m$ identity matrix

Equivalent formulation: There exists an invertible real matrix $P$ such that:
$P A P^{-1} = \begin{pmatrix} 0 & -I_m \\ I_m & 0 \end{pmatrix}$

This means that every real matrix whose square is $-I$ can be brought into a standard form consisting of $2 \times 2$ rotation blocks $\begin{pmatrix} 0 & -1 \\ 1 & 0 \end{pmatrix}$ along the diagonal, which represents a complex structure on $\mathbb{R}^n$ where $A$ acts as multiplication by the imaginary unit $i$.

[Nick_adfor]

Okay, as now new Aristotle has published, I'll try its new model with a .tex or other mathematical prompt

[Nick_adfor]

Just before I do not have a way to input my mathematical proof but now the new Aristotle version seems to have method to deal with it.

[Nick_adfor]

I'll try to see how it differs from ChatGPT.

[Yan Yablonovskiy 🇺🇦]

Nick_adfor said:

I'll try to see how it differs from ChatGPT.

This comment may interest you #Machine Learning for Theorem Proving > How have you guys found GPT 5? @ 💬

[Nick_adfor]

Okay, one month has passed and Aristotle has updated for many times. But it still cannot work out the problem.
With error:
/- Aristotle took a wrong turn (reason code: 0). Please try again. -/

[Nick_adfor]

I may think that what makes things bad is the complex definition about matrix. For the original math problem, there might be a lot of lean statement, they are all right, but there's one easier for Aristotle to check. Jordan decomposition seems necessary and I must write it by myself rather than make Aristotle generate it from air.