I would like to be able to do high-school level linear algebra in Lean/Mathlib. However, it seems pretty hard. I do understand that mathematicians don't care about being able to do this basic stuff but for teaching it should still work somehow?

My primary goal is learning how this basic stuff works so please feel free to change all the notation to be idiomatic. I also didn't find any documentation (neither in the books nor docs) on how to do something like this, glad about pointers!

Start with things that work

import Mathlib -- Mathlib4
open Real  -- start in in ℚ because ℝ is annoyingly noncomputable
open Matrix

--  0 1 2
--  1 3 5
--  2 5 8
def A : Matrix (Fin 3) (Fin 3) ℚ := 
    Matrix.of (fun i j ↦ (i.val + j.val) * (1 : ℚ) + i.val * j.val)

-- all ones
def B := Matrix.of !![(1 : ℚ), 1, 1; 1, 1, 1; 1, 1, 1]

#eval (A * B).det == (B * A).det -- true (both zero)
#eval (A * B).trace == (B * A).trace  -- true (both 27)

#eval Bᴴ == B  -- this just works, even though it's not `Decidable`?

#eval Aᴴ  -- the display could be nicer but OK

However, how can I...

lemma B_is_hermitian : Matrix.IsHermitian B := by
    sorry  -- just do the same thing as in the #eval?!

-- Doing it Manually... 
-- this is horrible and also insanely slow (due to the coercions?!)
lemma Ahermitian : Matrix.IsHermitian A := by
    have (x y : Fin 3) := calc (↑↑y : ℚ) + ↑↑x + ↑↑y * ↑↑x
        _ = ↑↑x + ↑↑y + ↑↑x * ↑↑y := by ring
    simp [IsHermitian]
    simp [transpose, A]
    ext x y
    repeat rw [this]

-- let's diagonalize B (over ℝ because need roots)

-- unitary matrix that diagonalizes B
noncomputable def U := 
!![ 1/sqrt 2, -1/sqrt 6, 1/sqrt 3 ;
    0       ,  2/sqrt 6, 1/sqrt 3 ;
   -1/sqrt 2, -1/sqrt 6, 1/sqrt 3 ]

example : U * Uᴴ = 1 := by
-- what I want to say is:
-- "perform matrix product, do `norm_num` componentwise"
    simp_all [U]
    -- ext m n  -- idea: prove equality of matrices as functions
    -- by considering all cases
    -- But this gives a huge mess, and I'm...

and finally

noncomputable def D := !![0, 0, 0; 0, 0, 0; 0, 0, 3]

-- Diagonalization. How do I coerce/convert `B` "from ℚ to ℝ"?
-- example : U * D * Uᴴ = ↑B := sorry

-- apply the general statement that U and D exist for A
-- this just TIMES OUT ?!?!
#check Matrix.IsHermitian.spectral_theorem Ahermitian
  • 1
    $\begingroup$ You are asking a sea of questions. I would argue that a site like this is not really appropriate for such questions and you need an interactive dialogue with Lean experts dealing with each point separately. Thus I would recommend that you re-ask this question on the Lean Zulip where people can go through and correct your misunderstandings and explain how to do what you want to do. Your claim that mathematicians don't care about being able to do this basic stuff is completely wrong; most of us in the Lean community teach and many of us want to see how to integrate Lean into our teaching. $\endgroup$ Oct 6, 2023 at 10:26
  • $\begingroup$ I would say that if you want to do linear algebra then a proof assistant is not the way to go at all! It's highly inefficient (at best) and is really not designed for that purpose! On the other hand, if you want to prove linear algebra theorems then Lean is the way to go. $\endgroup$ Oct 24, 2023 at 23:55
  • $\begingroup$ PS: Why do you expect to be able to do computation with a matrix that is explicitly marked as noncomputable? $\endgroup$ Oct 24, 2023 at 23:56
  • $\begingroup$ I'm not expecting #check to do the calculations using real numbers for me. However, it's clearly possible to reason about these matrices just like it's possible to reason about concrete (noncomputable) real numbers like Pi. So it's also perfectly possible to give a good answer to my question. There are places in math where you sometimes use a concrete number or a concrete matrix, so surely it's not a ridiculous notion that this should work in Lean. I get that most mathematicians don't need this and hence maybe nobody put in a lot of effort to make it easy to use. $\endgroup$ Oct 25, 2023 at 10:04
  • $\begingroup$ Clarification: I meant to say #eval, not #check, and also by "Pi is noncomputable" I meant that real numbers are marked noncomputable in Lean, not that Pi is an uncomputable real number. $\endgroup$ Oct 25, 2023 at 12:09


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Browse other questions tagged or ask your own question.