PR #31821 Singular Value Decomposition

Stream: PR reviews

[Levi G]

PR #31821 has definitions and proofs for Singular Value Decompositon. PR #31821

Here is the code designed for lean 4.25.0
SVD.txt

[Jireh Loreaux]

@Levi G did you work with @Niels Voss on this? It seems likely not.

[Kenny Lau]

@Jireh Loreaux no, he worked with GPT on this;
@Levi G your file needs to end in .lean for it to be a proper lean file

[Kenny Lau]

and you'll also need to do lake exe mk_all but you can do this later

[Jireh Loreaux]

Kenny, the PR passes CI (technically, but whatever)

[Jireh Loreaux]

(although I haven't looked at it past that)

[Jireh Loreaux]

oh, it passes CI because it's .txt

[Kenny Lau]

of course it passes CI, without .lean it isn't even a lean file (maybe that's how it works?)

[Damiano Testa]

Does lake exe mk_all work with the module system? At best, it will add "plain" imports, I guess.

[Kenny Lau]

Jireh Loreaux said:

Kevin, the PR passes CI

I don't see why that's a response to what i said, passing CI or not he still worked with GPT on this

[Jireh Loreaux]

Indeed, I've just closed the PR.

[Weiyi Wang]

Damiano Testa said:

Does lake exe mk_all work with the module system? At best, it will add "plain" imports, I guess.

It worked for me today after the module migration

[Levi G]

The code works though. Pls at least try it.

[Levi G]

@Jireh Loreaux I did not work with @Niels Voss

[Levi G]

@Jireh Loreaux Here is the file ending in .lean
I apologise for the confusion. I promise this ain't ai slop.
SVD.lean
@Kenny Lau Pls check and confirm.

[Anthony Wang]

The file you sent seems to have mangled Unicode characters, but I tried compiling your PR and surprisingly it does actually type check even though it's low quality AI slop.

[Levi G]

Wdym it's low quality AI slop? Maybe it is not well-written like a professional mathematician but doesn't it do the job and prove SVD for all complex matrices? It seems to work.

[Levi G]

Sorry and I apologise for the confusion about the whole txt thing. Lemme open another pr with the correct file extension.

[Levi G]

My new PR with the code using the right file extension ( .lean)

feat(Mathlib/Analysis): Existence of Singular Value Decomposition #31830

Pls @Jireh Loreaux and @Kenny Lau confirm.

[Aaron Liu]

You put lake exe mk_all at the top of the file

[Aaron Liu]

you were supposed to run it in the command line after saving the file, and then after it's done running commit the result

[Aaron Liu]

try deleting it from the file and run it in the command line instead

[Levi G]

Aaron Liu said:

you were supposed to run it in the command line after saving the file, and then after it's done running commit the result

Ahh ok thanks

[Levi G]

Aaron Liu said:

try deleting it from the file and run it in the command line instead

Thanks ... lemme do that

[Yan Yablonovskiy 🇺🇦]

Levi G said:

Wdym it's low quality AI slop? Maybe it is not well-written like a professional mathematician but doesn't it do the job and prove SVD for all complex matrices? It seems to work.

Simply doing the job is more relevant for your own purposes, but contributing to a repository is a lot more nuanced than that.

[Levi G]

(deleted)

[Jireh Loreaux]

@Levi G I did examine the PR before closing it. It may compile (which is more than can be said for a lot of the AI output we get here), but that's not nearly a high enough bar to qualify as a contribution to Mathlib.

However, I'll apologize for the way I handled it. I should have provided more of an explanation for why I was closing the PR. Let me do that now. I'll list a few of the more significant issues with this PR (although there are many more besides):

1. It only works for ℂ-valued matrices
2. It only works for matrices and not linear maps.
3. Your index sets are Fin n instead of arbitrary Fintypes
4. You don't link any of this to existing API (execpt for PosDef) in statements (e.g. you write V * Vᴴ = 1 ∧ Vᴴ * V =1). You don't use docs#Matrix.diagonal, docs#unitary, etc. in statements.
5. Your ratio of defs to lemmas is pretty high. Each definition introduced into the library needs sufficient API so that it is usable. Moreover, many of these are definitions we don't want, at least not in this form.
6. Your set_options and local instances at the top of the file are no good.
7. In part because of the above issues, the proofs of some key results are monstrously huge.

If you want to contribute to Mathlib, chat about your project on Zulip first, learn a lot, learn what's needed and how to go about things. After those steps, you'll be in a better state to contribute. I suggest not using an LLM, at least not to start, as it can prevent you from learning well.

[Moritz Doll]

As for 7: the proofs are also huge because they prove a things in a very roundabout way that no human would ever come up with. For example

have hmem : ∃ j₀, Fin.castLE h j = Fin.castLE h j₀ := ⟨j, rfl⟩
simp only [hmem, dif_pos]
congr 1
ext k
have h_spec : Classical.choose hmem = j := by
  have : Fin.castLE h (Classical.choose hmem) = Fin.castLE h j := (Classical.choose_spec hmem).symm
  exact Fin.castLE_injective h this
rw [h_spec]

at around line 707 in your current PR. Without even trying to understand what is going on here, I can tell that this is bad.

[Levi G]

Jireh Loreaux said:

Levi G I did examine the PR before closing it. It may compile (which is more than can be said for a lot of the AI output we get here), but that's not nearly a high enough bar to qualify as a contribution to Mathlib.

However, I'll apologize for the way I handled it. I should have provided more of an explanation for why I was closing the PR. Let me do that now. I'll list a few of the more significant issues with this PR (although there are many more besides):

1. It only works for ℂ-valued matrices
2. It only works for matrices and not linear maps.
3. Your index sets are Fin n instead of arbitrary Fintypes
4. You don't link any of this to existing API (execpt for PosDef) in statements (e.g. you write V * Vᴴ = 1 ∧ Vᴴ * V =1). You don't use docs#Matrix.diagonal, docs#unitary, etc. in statements.
5. Your ratio of defs to lemmas is pretty high. Each definition introduced into the library needs sufficient API so that it is usable. Moreover, many of these are definitions we don't want, at least not in this form.
6. Your set_options and local instances at the top of the file are no good.
7. In part because of the above issues, the proofs of some key results are monstrously huge.

If you want to contribute to Mathlib, chat about your project on Zulip first, learn a lot, learn what's needed and how to go about things. After those steps, you'll be in a better state to contribute. I suggest not using an LLM, at least not to start, as it can prevent you from learning well.

@Jireh Loreaux Thank you for your feedback and response. Feedback noted. I have a lot to learn. For this new PR I'll make the necessary changes based on your highlighted points.

[Levi G]

I have made quite a few extensive changes to my code, should be much better. Now my .lean code on github now passes all the tests. Please have a look. @Weiyi Wang @Aaron Liu @Jireh Loreaux

[Kenny Lau]

where?

[Levi G]

Kenny Lau said:

where?

Here: https://github.com/leanprover-community/mathlib4/pull/31830

feat(Mathlib/Analysis): Existence of Singular Value Decomposition #31830

[Kenny Lau]

did you (not gpt) even read through any of the points that Jireh presented above?

[Levi G]

Kenny Lau said:

did you (not gpt) even read through any of the points that Jireh presented above?

I have not finished everything especially the linear map instead of matrix and fintype S

[Levi G]

I wanted to get a minimal working clean version of the one with Complex Matrices before generalizing further because the previous had a boat load of issues even if it compiled.

[Kenny Lau]

that's great to hear, i look forward to it

[Michael Rothgang]

At the very least, let me mark your PR as awaiting-author then: this tells other reviewers that you're still working on it.edit: it already was
If you're done, you want write a comment with just the words -awaiting-author to remove that label.

[Levi G]

In particular I was handling points 4 to 7

Levi G said:

I wanted to get a minimal working clean version of the one with Complex Matrices before generalizing further because the previous had a boat load of issues even if it compiled.

[Michael Rothgang]

The current code still has a number of instances of (4) - while you're claiming they're solved. For me, that does not inspire confidence.

[Levi G]

Michael Rothgang said:

At the very least, let me mark your PR as awaiting-author then: this tells other reviewers that you're still working on it. If you're done, you want write a comment with just the words -awaiting-author to remove that label.

Ok thanks. Though it had been already marked.

[Levi G]

Michael Rothgang said:

The current code still has a number of instances of (4) - while you're claiming they're solved. For me, that does not inspire confidence.

Sorry still needs some work.

[Jireh Loreaux]

@Levi G please give up on this PR (and SVD) for now. I'm not saying you can't be a contributor to Mathlib, but it's going to take time to get there.

This is especially true for this material, as there is already someone (Niels Voss, which is why I asked about him earlier) who is working on this, and with whom we have had extensive discussions about design for singular values and the singular value decomposition. For example, one thing I didn't mention above is that your singular values only work for finite dimensional objects, but ultimately we'd like the entire singular value list even for compact operators in infinite dimensions.

If you honestly want to contribute to Mathlib, pick a small thing to do (let's say that the total code included in the PR for it should be < 75 lines or so). Mention it on Zulip before creating the PR and get feedback to make sure the contribution is welcome and your approach is a good idea. Then create the PR, get reviews, and pay careful attention to the feedback so you can learn for next time.

[Jireh Loreaux]

The extensive discussions I mentioned are here: #Is there code for X? > Singular Value Decomposition . I encourage you to read that thread, not so that you can be ready to contribute SVD, but so that you can learn the kinds of considerations that go into curating material for Mathlib, and see an example of how to ask on Zulip for feedback before creating a PR.

[Levi G]

Ok, understood. Thanks, Lemme close the PR on github.

[Jireh Loreaux]

Thanks for responding appropriately and taking the feedback constructively.

[Levi G]

Jireh Loreaux said:

The extensive discussions I mentioned are here: #Is there code for X? > Singular Value Decomposition . I encourage you to read that thread, not so that you can be ready to contribute SVD, but so that you can learn the kinds of considerations that go into curating material for Mathlib, and see an example of how to ask on Zulip for feedback before creating a PR.

Thank you for linking the thread. I will definitely go through it.

[Levi G]

Hello. I know we are supposed to discuss and come up with proofs in small chunks but right I have something significantly better than what I had before - a basis-free SVD for LinearMap over Real or Complex field. I would like to share that progress. But it’s for finite dimensional inner product spaces not the infinite dimensional case. Would that be of use/interest? I would like to hear your feedback. @Jireh Loreaux @Michael Rothgang @Weiyi Wang @Kenny Lau @Moritz Doll @Aaron Liu @Yan Yablonovskiy 🇺🇦

[Levi G]

Here it is. I would like to hear your feedback.
finite dimensional Basis-Free SVD-2.lean

[Levi G]

Any feedback? I know discussions are going on in other SVD thread but I just need some feedback.

[Johan Commelin]

@Levi G Let me put this bluntly: it is time to stop working on formalizing SVD now, and first take on smaller projects.

People have kindly invested time and energy into your earlier PRs, and have given you constructive feedback.
They also made clear that formalizing SVD is a minefield. Take that to heart.

[Levi G]

Johan Commelin said:

Levi G Let me put this bluntly: it is time to stop working on formalizing SVD now, and first take on smaller projects.

People have kindly invested time and energy into your earlier PRs, and have given you constructive feedback.
They also made clear that formalizing SVD is a minefield. Take that to heart.

@Johan Commelin Understood. It's just that I was hoping for some more feedback because this latest version is significantly better than anything that I had given before and also attempted to address their feedback. I hope you can at least take a look at this one. However, I have understood your point, it is a minefield so I will just stop pressing on this matter, hold-off completely and move on to other projects. Thank you for your feedback.

[Michael Rothgang]

I appreciate you trying to learn from feedback, and understand your wish for confirmation if you addressed it well! That said: at least I personally prefer giving feedback where it's directly useful --- by which I mean "I'd rather give you feedback on a different PR that's useful than on this one". As said above, #31821 will not get merged into mathlib, so any comments there would be only for your learning.
Commenting on a future PR of yours that has chances of making it to mathlib is a much better use of everybody's time. If you show willingness to learn, people are usually very happy to provide feedback.

[Nick_adfor]

Is there any Jordan decomposition in linear algebra? I search it and there's only Jordan decomposition in measure theory. Is it another minefield?