# Zulip Chat Archive

## Stream: new members

### Topic: What next?

#### Dustin Mixon (Oct 14 2021 at 02:05):

I played through NNG and solved the Lean maths challenges, and I'm hooked. What's the next step? I doubt I'm ready to formalize stuff seriously. Is there a "game" that teaches term mode? (I assume that's important??) Eventually, I may want to contribute to mathlib, but I wouldn't want to step on anyone's toes or reproduce effort. Is there a place I can go to see what needs to be done and who's doing what?

#### Bryan Gin-ge Chen (Oct 14 2021 at 02:35):

Welcome! We've got a bunch of different learning resources here, though I don't know of any other completed "games" like the NNG: https://leanprover-community.github.io/learn.html

We have a bunch of issues on the mathlib repo that you can take a look at, but the best way to find out if something's being worked on or not is to ask here on Zulip!

#### Scott Morrison (Oct 14 2021 at 04:36):

Typically the way to get started is to pick some random bit of maths that you like, and ask here what's been done on it. We can then try to steer you in the direction of something both plausible and useful. But it helps if you have some suggestion about the general areas of mathematics/CS that you're interested in.

#### Francis Southern (Oct 14 2021 at 09:04):

I'm in a similar situation. I did the NNG yesterday and I've just set up Lean and Emacs and now I'm working through the M40001 exercise sheets. I've got some fairly specific maths in mind that I'd like to formalise (related to my PhD project), but at the moment I have no idea how to even write definitions in Lean...

#### Johan Commelin (Oct 14 2021 at 09:06):

@Francis Southern Can you give an example of what you would like to define?

#### Johan Commelin (Oct 14 2021 at 09:06):

There are several ways to define things in Lean. Maybe the LftCM videos can help you?

#### Johan Commelin (Oct 14 2021 at 09:07):

https://www.youtube.com/watch?v=8mVOIGW5US4&list=PLlF-CfQhukNlxexiNJErGJd2dte_J1t1N

#### Francis Southern (Oct 14 2021 at 09:17):

Thanks for the suggestion, I'll definitely watch the videos, but I don't believe the objects I'm working with should be very complex. I'm in combinatorics, so basically I want specific types of (multi-)hypergraphs. It's fine to represent the vertices as pairs natural numbers. So I want a set S of all finite (multi-)sets of finite (multi-)sets of pairs of natural numbers. and then I want operations from S to S which add and remove edges and the like, and I want functions from S to $\mathbb{N}$ which give me various properties of the hypergraphs, like the number of times a certain vertex (pair of natural numbers) appears. Does that make sense?

#### Johan Commelin (Oct 14 2021 at 09:30):

"all finite multisets of finite multisets of pairs of natural numbers" would be

```
multiset (multiset (ℕ × ℕ))
```

#### Johan Commelin (Oct 14 2021 at 09:31):

So you could do something like

```
def specific_type_of_hypergraph := multiset (multiset (ℕ × ℕ))
```

#### Johan Commelin (Oct 14 2021 at 09:32):

And then

```
def specific_type_of_hypergraph.count_vertex : specific_type_of_hypergraph → ℕ :=
_ -- fill this in
```

#### Yaël Dillies (Oct 14 2021 at 09:36):

I've added you to the stream graph theory.

#### Francis Southern (Oct 14 2021 at 09:38):

Johan Commelin said:

"all finite multisets of finite multisets of pairs of natural numbers" would be

`multiset (multiset (ℕ × ℕ))`

Thank you, that's very helpful. How would I then refer to the set of all specific_type_of_hypergraphs? And how could I make subsets of that set?

#### Francis Southern (Oct 14 2021 at 09:38):

Yaël Dillies said:

I've added you to the stream graph theory.

Thank you. :-)

#### Johan Commelin (Oct 14 2021 at 09:41):

@Francis Southern `specific_type_of_hypergraphs`

*is* the collection/set/type of all such hypergraphs.

#### Johan Commelin (Oct 14 2021 at 09:42):

So you can write `variable (G : specific_type_of_hypergraphs)`

to say "Let `G`

be a (specific type) hypergraph".

#### Johan Commelin (Oct 14 2021 at 09:42):

Do these specific type of hypergraphs have a specific name? Of course `specific_type_of_hypergraph`

is a bit awkard, and way too long to be practical.

#### Johan Commelin (Oct 14 2021 at 09:43):

Note that Lean is based on type theory. So you will find less talk about sets, and more talk about types. But from a practical point of view (as mathematician), the difference is not important.

#### Johan Commelin (Oct 14 2021 at 09:44):

`ℕ`

and `ℝ`

are types. But `{π, √2}`

is a set of real numbers.

#### Johan Commelin (Oct 14 2021 at 09:44):

So in Lean you can basically only talk about *subsets*. If you want an "ambient" set, then you should use types instead.

#### Johan Commelin (Oct 14 2021 at 09:45):

The collection of all hypergraphs is naturally a type. It's the collection of all hypergraphs. Just like `ℕ`

is the collection of all natural numbers.

#### Francis Southern (Oct 14 2021 at 10:05):

Oh, whoops. I see. But if, for example, I want the set of all positive real numbers or hypergraphs with exactly k vertices? I suppose I mean how do I write set (type?) comprehension?

And regarding naming, we could call them "generalised clause sets" as they are a generalisation of boolean clause sets (generalised because variables may take more than two values, and also because I'm considering multisets of clauses which can actually contain "clashing literals"). These changes make the setting more combinatorial than logical though.

#### Francis Southern (Oct 14 2021 at 10:06):

I'm not sure these objects are of a particularly general interest though, so they don't really have a short or precise name, so far as I know (I'd love to be proved wrong on that though!).

#### Yaël Dillies (Oct 14 2021 at 10:06):

See docs#nnreal and docs#subtype.

#### Yaël Dillies (Oct 14 2021 at 10:06):

The idea is that you can create a new type by carving it out a previous one using its indicator predicate.

#### Francis Southern (Oct 14 2021 at 10:07):

By the way, am I mistaken or did the definitions you give earlier, Johan, make no reference to finiteness?

#### Johan Commelin (Oct 14 2021 at 10:07):

```
def positive_set : set ℝ := {x | 0 < x}
def positive_subtype : Type := {x : ℝ // 0 < x}
-- assumes `hypergraph.count_vertices` is defined
def with_vertices (k : ℕ) : set hypergraph := {G | G.count_vertices = k}
```

#### Yaël Dillies (Oct 14 2021 at 10:07):

`multiset`

is, by definition, finite.

#### Francis Southern (Oct 14 2021 at 10:07):

Ah, that looks perfect, Yaël. I hadn't seen this documentation yet. I'm sorry being such a neophyte. :-)

#### Johan Commelin (Oct 14 2021 at 10:08):

The distinction between `set`

and `subtype`

is a bit painful, unfortunately.

#### Johan Commelin (Oct 14 2021 at 10:08):

No worries! We've all been newbies. And there is quite a lot to learn.

#### Yaël Dillies (Oct 14 2021 at 10:08):

If you want an infinite multiset, you just do `α → ℕ`

.

#### Johan Commelin (Oct 14 2021 at 10:08):

We are always interested in taming the learning curve.

#### Francis Southern (Oct 14 2021 at 10:09):

Thanks again, I really appreciate it! I'll now sit and read and watch and digest a bit.

#### Dustin Mixon (Oct 14 2021 at 11:14):

One thing I'm interested in is formalizing the main result in [HM18]. This is the state of the art for the Paulsen problem in frame theory. Recently, a colleague identified a tiny (presumably inconsequential) error in the proof, so I'd like to regain full confidence. The proof uses Theorem 4.1 in Forster's "A linear lower bound on the unbounded error probabilistic communication complexity", which in turn uses tools from matrix analysis (e.g., the spectral theorem for real symmetric matrices, the fact that singular values depend continuously on the matrix, etc.). How far is matrix analysis from today's mathlib?

#### Yaël Dillies (Oct 14 2021 at 11:16):

Tip: Ctrl + Shift + L to insert a link :wink:

#### Johan Commelin (Oct 14 2021 at 12:18):

@Dustin Mixon I think that such matrix analysis is certainly within reach. @Heather Macbeth might want to chime in.

#### Heather Macbeth (Oct 14 2021 at 13:35):

We will have the (finite-dimensional) spectral theorem quite soon! The fact that the singular values depend on the matrix would be very nice to have; I guess one of the ingredients would be the implicit function theorem, which is in mathlib, but another would be the continuity of the determinant, which was mentioned just the other day as a TODO:

https://leanprover.zulipchat.com/#narrow/stream/303200-sphere-eversion/topic/Smoothness.20of.20barycentric.20coordinates.20.28Lemma.201.2E7.29

Last updated: Dec 20 2023 at 11:08 UTC