Vectors & matrices in Lean

Stream: general

[Andrew Helwer]

Can anyone point me to where & how vectors & matrices are defined in lean?

[Simon Hudon]

In mathlib data.matrix.basic

[Andrew Helwer]

Are there good examples anywhere for the basics of how to use & manipulate this definition?

[Johan Commelin]

No I'm afraid... we don't have much linalg in terms of matrices...

[Johan Commelin]

So your best bet is to read that file (and PR some docs if you want/can!)

[Johan Commelin]

Also, you can search for data.matrix.basic to see which files import the definition of matrix

[Patrick Massot]

Or else you can have a look at the output of leanproject import-graph --from data.matrix.basic matrix.pdf

[Patrick Massot]

The fact that ring_theory.algebra import matrices is a bit misleading...

[Bryan Gin-ge Chen]

I suppose one could fire up leancrawler and look for declarations that actually rely on the matrix definition...

[Patrick Massot]

True.

[Patrick Massot]

Merging leanproject, format_lean and leancrawler is still on my TODO list...

[Ryan Lahfa]

Patrick Massot said:

Merging leanproject, format_lean and leancrawler is still on my TODO list...

Wow, leancrawler looks amazing

[Patrick Massot]

This is what produced the big graph at https://leanprover-community.github.io/lean-perfectoid-spaces/

[Ryan Lahfa]

I really liked this graph and wondered if I could produce snapshots of those for arbitrary theorem in mathematics

[Patrick Massot]

This will be much easier when leancrawler will be part of leanproject. But this requires time, and I'm already spending way too much time on Lean tooling.

[Ryan Lahfa]

Patrick Massot said:

This will be much easier when leancrawler will be part of leanproject. But this requires time, and I'm already spending way too much time on Lean tooling.

I'm quite proficient in Python, is there a way to give a hand?

[Patrick Massot]

The current blocking stuff is on the Lean meta-programming side I'm afraid.

[Ryan Lahfa]

@Patrick Massot Well, I'm interested into looking at the C++ internals of Lean, but not now, I don't have enough confidence on such piece of software :)

[Patrick Massot]

This has nothing to do with C++.

[Ryan Lahfa]

Patrick Massot said:

This has nothing to do with C++.

You mean the meta-programming in Lean (e.g. tactics building, etc.) ?

[Patrick Massot]

Yes.

[Ryan Lahfa]

Patrick Massot said:

Yes.

Are there any docs beyond tactics writing (which I know I already asked you about it) on the general meta-programming language/engine? I have seen that Lean 4 has something which looks a bit what Rust has for macros and I'm used to these kinds of meta-programming stuff

[Scott Morrison]

@Ryan Lahfa , what have you read already? https://doi.org/10.1145/3110278 is a great start.

[Ryan Lahfa]

Scott Morrison said:

Ryan Lahfa , what have you read already? https://doi.org/10.1145/3110278 is a great start.

Nothing more than Lean reference manual https://leanprover.github.io/reference/lean_reference.pdf and the mathlib docs. Will bookmark this :) — thank you!

[Sebastien Gouezel]

I just tried leanproject import-graph (on my windows machine), and I get (from a powershell shell)

PS C:\Users\Sebastien\Desktop\mathlib> leanproject import-graph --from data.fintype.basic fintype.pdf
[WinError 2] "dot" not found in path.

and from a Cygwin shell

Sebastien@DESKTOP-51UASBS /cygdrive/c/Users/Sebastien/Desktop/mathlib
$ leanproject import-graph --from data.fintype.basic fintype.pdf
expected string or bytes-like object

[Yury G. Kudryashov]

It needs dot from graphviz to produce pdfs

[Sebastien Gouezel]

OK, let me install graphviz and report back. Thanks!

[Yury G. Kudryashov]

fintype-graph.pdf

[Yury G. Kudryashov]

Do you want to remove something from this graph?

[Sebastien Gouezel]

Works like a charm, thanks!

[Kevin Buzzard]

I hope this graph clarifies whatever you were wondering about :-)

[Sebastien Gouezel]

With the right --from and the right --to, yes, the tool is extremely informative.