What next?

Stream: new members

[Dustin Mixon]

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]

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]

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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Francis Southern]

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]

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

multiset (multiset (ℕ × ℕ))

[Johan Commelin]

So you could do something like

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

[Johan Commelin]

And then

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

[Yaël Dillies]

I've added you to the stream graph theory.

[Francis Southern]

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]

Yaël Dillies said:

I've added you to the stream graph theory.

Thank you. :-)

[Johan Commelin]

@Francis Southern specific_type_of_hypergraphs is the collection/set/type of all such hypergraphs.

[Johan Commelin]

So you can write variable (G : specific_type_of_hypergraphs) to say "Let G be a (specific type) hypergraph".

[Johan Commelin]

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]

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]

ℕ and ℝ are types. But {π, √2} is a set of real numbers.

[Johan Commelin]

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

[Johan Commelin]

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]

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]

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]

See docs#nnreal and docs#subtype.

[Yaël Dillies]

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

[Francis Southern]

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

[Johan Commelin]

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]

multiset is, by definition, finite.

[Francis Southern]

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

[Johan Commelin]

The distinction between set and subtype is a bit painful, unfortunately.

[Johan Commelin]

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

[Yaël Dillies]

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

[Johan Commelin]

We are always interested in taming the learning curve.

[Francis Southern]

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

[Dustin Mixon]

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]

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

[Johan Commelin]

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

[Heather Macbeth]

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