Actual graph

Stream: condensed mathematics

[Patrick Massot]

I should have done that yesterday night to get it ready for the party, but I was stuck with primitives of integrable functions. Tonight I managed to bugfix leancrawler thanks to @Jesse Michael Han's I/O advice and generated a couple of graphs, including
final_graph.png

[Patrick Massot]

Remember this is what human being think is the project dependency graph. The picture above is Lean's point of view.

[Patrick Massot]

Of course the big graph includes everything needed from mathlib (and even the core library).

[Patrick Massot]

Each node is either a definition or a lemma (instances included).

[Patrick Massot]

I tried to write a poll to see who could guess how many nodes there are, but I can't get it to work.

[Patrick Massot]

Johan do you know how to make a Zulip poll that work?

[Patrick Massot]

Some of those nodes are a bit surprising. Who knows why docs#ordinal is involved?

[Johan Commelin]

/poll title
- option 1
- option 2

[Patrick Massot]

Can you preview it when you write it?

[Patrick Massot]

Because I tried that and then clicked the preview button and never see my poll

[Johan Commelin]

/poll Which city in France represents the vertex first_target

• Paris
• Marseille
• Nancy
• Lille
• Bordeaux

[Patrick Massot]

/poll How many nodes?
1000
4000
8000
12000
15000
20000

[Patrick Massot]

/poll How long is the longest (directed) path in this graph?
between 10 and 50
between 50 and 100
between 100 and 150

[Patrick Massot]

Free form question: why is docs#complex.cosh_neg involved?!

[Patrick Massot]

(Shameless self-advertisement: leancrawler does know all the answers)

[Sebastien Gouezel]

Patrick Massot said:

Free form question: why is docs#complex.cosh_neg involved?!

It is not involved and you're just playing with us. Right? How else could it be :-)

[Patrick Massot]

Sébastien I can see your understanding of condensed mathematics is not so deep. Then you'll be surprised when it will replace topology and analysis.

[Peter Scholze]

Actually, why the heck is that involved??

[Patrick Massot]

And then Peter will come along and ask why cosh is involved at all, and maybe we'll reconsider how we prove things in mathlib

[Patrick Massot]

Oh, here he is

[Peter Scholze]

Did you make the graph look like France on purpose?

[Patrick Massot]

It's all automatically generated by gephi. Johan and Kevin saw it live, they can testify I didn't change anything

[Johan Commelin]

/poll How many edges are there in the graph?

• between 10,000 and 20,000
• between 20,000 and 40,000
• between 40,000 and 80,000
• between 80,000 and 125,000
• between 125,000 and 175,000

[Sebastien Gouezel]

Patrick Massot said:

Sébastien I can see your understanding of condensed mathematics is not so deep. Then you'll be surprised when it will replace topology and analysis.

I can confirm that my understanding of condensed mathematics is not so deep. And that I'll be very surprised if it replaces topology and analysis (but I guess you'll have a hard time convincing people that condensed Sobolev spaces are the way to go :-)

[Sebastien Gouezel]

(unless you explain that wavelets are a version of condensed mathematics, which is possibly something that could be argued for)

[Patrick Massot]

Let's go back to serious mathematics and comtemplate the path from cosh_neg to first_target:

In [36]: nx.shortest_path(gr, 'complex.cosh_neg', 'first_target')
Out[36]:
['complex.cosh_neg',
 'complex.cos_conj',
 'complex.of_real_cos_of_real_re',
 'complex.of_real_cos',
 'complex.exp_log',
 'complex.cpow_one',
 'complex.cpow_nat_cast',
 'real.rpow_nat_cast',
 'nnreal.rpow_nat_cast',
 'thm95.universal_constants.N₂_spec',
 "thm95.universal_constants.k'_le_two_pow_N",
 'NSH_δ',
 "NSH_aux'",
 'NSH_aux',
 'NSC_htpy',
 'NSC',
 "thm95'",
 "thm95''",
 'first_target']

[Patrick Massot]

It obviously goes through docs#real.rpow_nat_cast

[Patrick Massot]

whose importance cannot be overestimated and whose proof obviously uses cosh

[Patrick Massot]

More generally, the definition of a real number raised to a real power is what drags in all of trigonometry, through log and exp

[Peter Scholze]

Don't you only ever need natural number powers of real numbers?

[Patrick Massot]

It also features in the longest path of the graph:

In [40]: nx.dag_longest_path(gr)
Out[40]:
['nat',
 'nat.less_than_or_equal',
 'nat.has_le',
 'nat.le_refl',
 'nat.pred_le_pred',
 'nat.le_of_succ_le_succ',
 'nat.not_succ_le_self',
 'nat.lt_irrefl',
 'nat.lt_iff_le_not_le',
 'nat.linear_order',
 'nat.le_of_sub_eq_zero',
 'int.sub_nat_nat_elim',
 'int.sub_nat_nat_add_add',
 'int.sub_nat_nat_sub',
 'int.sub_nat_nat_add_neg_succ_of_nat',
 'int.add_assoc_aux2',
 'int.add_assoc',
 'int.le.dest',
 'int.le.elim',
 'int.lt.dest',
 'int.lt.elim',
 'int.lt_irrefl',
 'int.ne_of_lt',
 'int.lt_iff_le_and_ne',
 'int.lt_iff_le_not_le',
 'int.linear_order',
 'int.linear_ordered_comm_ring',
 'int.linear_ordered_add_comm_group',
 'int.zero_div',
 'int.mod_add_div',
 'int.mod_def',
 'int.add_mul_mod_self',
 'int.mul_mod_left',
 'int.mul_mod_right',
 'int.mod_eq_zero_of_dvd',
 'int.div_mul_cancel',
 "int.mul_div_cancel'",
 'int.eq_mul_of_div_eq_right',
 'int.eq_mul_of_div_eq_left',
 'rat.mk_eq',
 'rat.lift_binop_eq',
 'rat.mul_def',
 'rat.mul_comm',
 'rat.mul_add',
 'rat.field',
 'rat.division_ring',
 'rat.add_comm_group',
 'rat.add_group',
 'rat.le',
 'rat.has_le',
 'rat.le_trans',
 'rat.linear_order',
 'rat.linear_ordered_field',
 'rat.linear_ordered_comm_ring',
 'rat.linear_ordered_ring',
 'rat.linear_ordered_add_comm_group',
 'real',
 'real.has_mul',
 'real.comm_ring',
 'real.ring',
 'real.semiring',
 'real.of_rat',
 'real.of_rat_lt',
 'real.zero_lt_one',
 'real.nontrivial',
 'real.linear_ordered_comm_ring',
 'real.linear_ordered_field',
 'real.field',
 'nnreal.has_div',
 'nnreal.comm_group_with_zero',
 'nnreal.linear_ordered_comm_group_with_zero',
 'real.to_nnreal_eq_zero',
 'real.to_nnreal_mul',
 'real.sqrt_mul',
 'complex.abs_mul',
 'complex.abs_add',
 'complex.abs.is_absolute_value',
 'complex.abs_div',
 'complex.is_cau_abs_exp',
 'complex.is_cau_exp',
 "complex.exp'",
 'complex.exp',
 'complex.exp_add',
 'complex.exp_ne_zero',
 'complex.exp_neg',
 'complex.cosh_neg',
 'complex.cos_conj',
 'complex.of_real_cos_of_real_re',
 'complex.of_real_cos',
 'real.cos_bound',
 'real.cos_pos_of_le_one',
 'real.cos_one_pos',
 'real.cos_two_neg',
 'real.exists_cos_eq_zero',
 'real.pi',
 'real.cos_pi_div_two',
 'real.cos_pi',
 'real.sin_pi_sub',
 'real.sin_pos_of_pos_of_lt_pi',
 'real.sin_pi_div_two',
 'real.sin_add_pi_div_two',
 'real.cos_pos_of_mem_Ioo',
 'real.cos_neg_of_pi_div_two_lt_of_lt',
 'real.cos_lt_cos_of_nonneg_of_le_pi',
 'real.sin_lt_sin_of_lt_of_le_pi_div_two',
 'real.strict_mono_incr_on_sin',
 'real.sin_order_iso',
 'real.arcsin',
 'complex.arg',
 'complex.log',
 'complex.cpow',
 'complex.has_pow',
 'real.rpow',
 'real.has_pow',
 'real.rpow_def',
 'real.rpow_def_of_nonneg',
 'real.rpow_def_of_pos',
 'real.rpow_pos_of_pos',
 'real.log_rpow',
 'real.log_pow',
 'helper.N₂_spec',
 'thm95.universal_constants.N₂_spec',
 "thm95.universal_constants.k'_le_two_pow_N",
 'NSH_δ',
 "NSH_aux'",
 'NSH_aux',
 'NSC_htpy',
 'NSC',
 "thm95'",
 "thm95''",
 'first_target']

[Patrick Massot]

We use real powers in the constants quest

[Patrick Massot]

'thm95.universal_constants.N₂_spec' is the begin of LTE in this path from cosh_neg to first_target

[Johan Commelin]

Hmm, but actually we can maybe avoid taking real powers there.

[Patrick Massot]

See here

[Johan Commelin]

We are using a lemma that is true for real powers, but we can probably specialize it to nat-powers

[Peter Scholze]

OK, I see

[Patrick Massot]

Of course we're actually defining a natural number there

[Peter Scholze]

So if I count it right, my answer to your second poll is correct!

[Patrick Massot]

I'm guilty here. Initially Johan had an abstract definition involving archimedianity (is that an English word?) and I fount it more convenient to simply put that actual minimal value there, because it meant less nested inductive definitions

[Patrick Massot]

Yes! the longest path has 131 vertices

[Patrick Massot]

And it goes from nat to first_target, which is pretty satisfying

[Adam Topaz]

Kronecker would be happy

[Patrick Massot]

Kronecker would be happy with the foundations we have. The variant of type theory that Lean uses is a variant of the calculus of inductive construction where inductive types (including natural numbers) are right at the bottom, not defined in term of anything else.

[Patrick Massot]

I guess there enough messages in this thread that we can post more answers to the polls without spoiling

[Patrick Massot]

There are 7859 nodes and more than 100.000 edges

[Patrick Massot]

I'm always amazed to see that those graphs are basically always a giant ball with some many edges compared to nodes.

[Patrick Massot]

And actually it could be much tighter, I always remove things that are too foundational like logic or set

[Patrick Massot]

It reminds me another fun question: what is the small green group that seems separated from the main blob on the top-right between the two pink areas?

[Johan Commelin]

The first_target vertex is close to Nancy (in the orange blob in the East)

[Patrick Massot]

What's interesting about this first_target node is it's completely surrounded by category theory

[David Michael Roberts]

Patrick Massot said:

Yes! the longest path has 131 vertices

That's still 53 steps shorter than the longest path in the Metamath proof of 2+2=4 ... :upside_down:

[Mario Carneiro]

Not sure who to credit for those additional steps (Cantor?) - most of the excess depth in the metamath proof is building up nat from set theory

[Damiano Testa]

This kind of data is really fascinating and something that I can only imagine doing after formalization!

Regarding the graph and its tightness, a different point of view is that it only has a small fraction of the edges that it could have: there are $\sim \! \binom{8000}{2} \approx 1.6 \cdot 10^7$ pairs of vertices, as opposed to $\approx 10^5$. (Unless, of course, when you said that it had more than 100.000 edges you really meant a lot more than 100.000! :upside_down: )

[Johan Commelin]

No, it's not a lot more. I don't remember the exact number, but it's less than 125,000.

[Mario Carneiro]

I think a better metric is to solve for $\alpha$ in $E\sim V^\alpha$

[Mario Carneiro]

A sparse graph has $\alpha\approx 1$ but I think this is higher

[David Michael Roberts]

Yeah, it's a bit of an apples/oranges comparison. But allowing for Metamath starting from set theory and getting basic arithmetic, and Lean starting from nat as an inductive type, but getting up to condensed mathematics (or near to it), it's at least anecdotally interesting.

[Mario Carneiro]

I think a lot of people draw the wrong conclusions from that factoid though, it's just a bit harmful

[Mario Carneiro]

for example, if you were to guess that it means that lean can get more done with less work, I think it's not true at all at the low level. There is a large fixed cost of setting up set theory, proving that functions exist etc, and then it's just a matter of the size of theorems. Metamath has more broken up proofs like foolem1, foolem2, ... foolem14, foo instead of having one huge theorem

[Yaël Dillies]

Oh wow! I picked up a random little off the graph, counted the number of nodes in there, then counted how many times I could fit it in, and got pretty pretty close!

[David Michael Roberts]

I'm trying not to draw a conclusion, just thought it was a randomly interesting fact.

[Peter Scholze]

So what do the colours actually represent in the graph?

[Johan Commelin]

I was trying to edit the picture to add some labels, but my graphics program is crashing :sad:

[Johan Commelin]

The colours are clusters calculated by gephi. There is a mild correspondence between these clusters and mathematical subfields

[Johan Commelin]

The orange blob in the east which contains first_target is a mix of semi_normed_group and category theory.

[Johan Commelin]

The big blob below it is a mix of algebra (groups/rings) and stuff about the reals.

[Peter Scholze]

Is all this stuff about profinite sets and Mbar and so on considered part of category theory?

[Johan Commelin]

In the south west, we get linear algebra. The blue peninsula in the west is stuff about finite discrete maths (lists/multisets/finsets). Then we get a small pink peninsula about ordinals/cardinals. Finally the big pinkish region in the north is topology.

[Johan Commelin]

Mbar and breen_deligne are scattered all over the place.

[Johan Commelin]

But note that vertices belonging to the project only make up a very small part of this graph. I don't have exact numbers, but my guess is it's < 15%.

[Johan Commelin]

The project is 20,000 lines of code, mathlib is more like 600,000. Of course we don't use all of mathlib. But I wouldn't be surprised if we use quite a fraction of mathlib.

[Johan Commelin]

I guess a bunch of profinite stuff is in the topology blob, but we didn't check yesterday night. Patrick can give more precise answers.

[Riccardo Brasca]

Wow, this is really fascinating! Where can I find out how you did it?

[Johan Commelin]

Patrick wrote a tool leancrawler which can generate (amongst other things) the data that gephi needs to generate this graph.

[Johan Commelin]

But I'm not an expert on this. I just watched his screen last night, while he was exploring the data

[Patrick Massot]

I'm away from my computer until dinner. I'll share more tonight. The version of leancrawler that is on github won't work because of issues in Lean3 IO and I didn't push the workaround yet.

[Riccardo Brasca]

Do someone have an idea of why ordinals are there?

[Johan Commelin]

Yeah, in the proof of 9.8 we need to show use that something is countable

[Johan Commelin]

I guess we can avoid it by writing down a hands-on equiv to nat. But I don't care too much

[Johan Commelin]

Or rather, in the proof of 9.8, we need a bijection $S \times \mathbb N \to \mathbb N$, where $S$ is finite. And I just pull one out of the hat using some lemma about cardinals.

[Johan Commelin]

final_graph_labels.png final_graph_labels.png.svg

[Johan Commelin]

My silly attempt at adding some labels to the graph

[Johan Commelin]

The somewhat correspond to reality.

[Johan Commelin]

If someone wants to do a better job (I'm terrible at this), I've posted the .svg above.

[Patrick Massot]

The functional analysis label is a bit random isn't it?

[Johan Commelin]

Yep, in reality it's basically mixed with category theory

[Johan Commelin]

The middle of the graph is a grab bag with lots of stuff. But there is a bit of functional analysis there, I think.

[Johan Commelin]

I'm open to other suggestions

[Patrick Massot]

The middle of the graph is just a mess.

[Johan Commelin]

So we replace the label with Mess? :stuck_out_tongue_wink:

[Patrick Massot]

The big dot below the a of analysis is add_monoid.to_add_zero_class...

[Johan Commelin]

Which is clearly one of the cornerstones of this proof :grinning:

[Peter Scholze]

It's like France: In the middle of it, there's just... stuff.

[Patrick Massot]

All the other big dots in this area are similar (like add_comm_group.to_add_group)

[Patrick Massot]

No, in the middle of France there is nothing at all.

[Johan Commelin]

Should we move the algebra label over there? And call the blue blob Real and complex numbers instead?

[Johan Commelin]

We want (Functional) analysis somewhere, I guess.

[Peter Scholze]

By the way, is it surprising or not that most nodes are very small?

[Johan Commelin]

The size of a node corresponds to the out-degree

[Johan Commelin]

Which means that most things get used just a couple of times.

[Peter Scholze]

sure... but this seems to indicate that there are very few nodes of large importance

[Johan Commelin]

Ooh, Patrick has cut away all the logic from this graph

[Peter Scholze]

I recall that the perfectoid spaces graph looked pretty different

[Johan Commelin]

Otherwise we would have one big mess, where everything is connected to basic logic lemmas that are not important.

[Johan Commelin]

Probably iff.mp would be one of the most used results or so.

[Peter Scholze]

It had some discernible structure (other than colors), and quite a few bigger nodes, I think

[Patrick Massot]

There are two kinds of large nodes. The first kind is what we just discussed. The second one is made of central actual definition, like real numbers or topological spaces.

[Peter Scholze]

Better than add_comm_group.to_add_group...

[Johan Commelin]

[Johan Commelin]

I'm not sure we can do much science on these graphs. As Patrick pointed out somewhere, the main benefits are
(1) They look really nice :octopus:
(2) An actual use case: we can now easily find out which definitions are in the dependency chain of the statement of the main theorem.

[Johan Commelin]

Fun fact: when Soergel (a prof in Freiburg) saw the graph for perfectoid spaces somewhere in 2019, he asked what consequences Brexit would have for Lists and Finite sets.

[Patrick Massot]

I think that one difference with the perfectoid graph is we added even more weird classes to the algebra hierarchy since then.

[Peter Scholze]

Actually, why was the key node large in the perfectoid graph? Or does it just overlap with a large node?

[Patrick Massot]

The key node had a special treatment, so that we can see it.

[Peter Scholze]

Ah, so you tricked me into believing that I should also look for a large node in the new graph

[Yaël Dillies]

I'm impressed at how the LTE graph is much denser than the perfectoid one. And I was already impressed by the latter! Now it looks quite sparse to me.

[Yaël Dillies]

Is it that the definition of perfectoids really uses much less, or is that an artifact of the graph presentation?

[Johan Commelin]

LTE has about 2x as many lines of lean code. It also imports more from mathlib.

[Johan Commelin]

final_graph_labels.png
Here's a version where the star has a more distinct colour.

[Adam Topaz]

What is the mixed in blueish-purple to the left of topology?

[Riccardo Brasca]

I am trying to make the graph now that the project is done, following the tutorial here. If someone is interested in the data produced by lib = LeanLib.load_dump('my_py_data') they're here data data.yaml.

But how am I supposed to make the graph? After G = LeanDeclGraph.from_lib(lib) it thinks a little bit, but no file is created. Should I save it somehow?

[Riccardo Brasca]

BTW here is the longest path

['nat',
 'nat.less_than_or_equal',
 'nat.has_le',
 'nat.le_refl',
 'nat.le_succ',
 'nat.le_succ_of_le',
 'nat.le_add_right',
 'nat.le.intro',
 'nat.add_le_add_left',
 'nat.add_le_add_right',
 'nat.le_of_sub_eq_zero',
 'int.sub_nat_nat_elim',
 'int.sub_nat_nat_add_add',
 'int.sub_nat_nat_sub',
 'int.sub_nat_nat_add_neg_succ_of_nat',
 'int.add_assoc_aux2',
 'int.add_assoc',
 'int.le.dest',
 'int.le.elim',
 'int.lt.dest',
 'int.lt.elim',
 'int.lt_irrefl',
 'int.ne_of_lt',
 'int.lt_iff_le_and_ne',
 'int.lt_iff_le_not_le',
 'int.linear_order',
 'int.linear_ordered_comm_ring',
 'int.add_mul_div_right',
 'int.add_mul_mod_self',
 'int.mul_mod_left',
 'int.mul_mod_right',
 'int.mod_eq_zero_of_dvd',
 'int.div_mul_cancel',
 "int.mul_div_cancel'",
 'int.eq_mul_of_div_eq_right',
 'int.eq_mul_of_div_eq_left',
 'rat.mk_eq',
 'rat.lift_binop_eq',
 'rat.mul_def',
 'rat.mul_comm',
 'rat.mul_add',
 'rat.field',
 'rat.division_ring',
 'rat.add_comm_group',
 'rat.add_group',
 'rat.le',
 'rat.has_le',
 'rat.le_trans',
 'rat.linear_order',
 'rat.linear_ordered_field',
 'rat.linear_ordered_comm_ring',
 'rat.linear_ordered_ring',
 'real',
 'real.has_zero',
 'real.of_cauchy_zero',
 'real.mk_zero',
 'real.mk_pos',
 'real.mul_pos',
 'real.ordered_comm_ring',
 'real.ordered_ring',
 'real.ordered_semiring',
 'nnreal.ordered_semiring',
 'nnreal.sqrt',
 'nnreal.sqrt_eq_iff_sq_eq',
 'nnreal.sqrt_eq_zero',
 'nnreal.sqrt_zero',
 'real.sqrt_zero',
 'real.sqrt_eq_zero',
 'complex.abs_eq_zero',
 'complex.abs.is_absolute_value',
 'complex.abs_div',
 'complex.is_cau_abs_exp',
 'complex.is_cau_exp',
 "complex.exp'",
 'complex.exp',
 'complex.exp_add',
 'complex.exp_ne_zero',
 'complex.exp_neg',
 'complex.cosh_neg',
 'complex.cos_conj',
 'complex.of_real_cos_of_real_re',
 'complex.cos_of_real_im',
 'complex.exp_of_real_mul_I_im',
 'real.cos_bound',
 'real.cos_pos_of_le_one',
 'real.cos_one_pos',
 'real.cos_two_neg',
 'real.exists_cos_eq_zero',
 'real.pi',
 'real.cos_pi_div_two',
 'real.cos_pi',
 'real.sin_antiperiodic',
 'real.sin_pi_sub',
 'real.sin_pos_of_pos_of_lt_pi',
 'real.sin_pi_div_two',
 'real.sin_add_pi_div_two',
 'real.cos_pos_of_mem_Ioo',
 'real.cos_neg_of_pi_div_two_lt_of_lt',
 'real.cos_lt_cos_of_nonneg_of_le_pi',
 'real.sin_lt_sin_of_lt_of_le_pi_div_two',
 'real.strict_mono_on_sin',
 'real.sin_order_iso',
 'real.arcsin',
 'real.arcsin_mem_Icc',
 'real.arcsin_eq_of_sin_eq',
 'real.arcsin_neg_one',
 'real.arcsin_of_le_neg_one',
 'real.arcsin_neg',
 'complex.sin_arg',
 'complex.abs_mul_exp_arg_mul_I',
 'complex.abs_mul_cos_add_sin_mul_I',
 'complex.arg_mem_Ioc',
 'complex.arg_real_mul',
 'complex.arg_eq_pi_iff',
 'complex.arg_of_real_of_neg',
 'real.rpow_def_of_neg',
 'real.abs_rpow_le_abs_rpow',
 'real.abs_rpow_le_exp_log_mul',
 'real.continuous_at_rpow_of_pos',
 'real.continuous_at_rpow',
 'nnreal.continuous_at_rpow',
 'filter.tendsto.nnrpow',
 'nnreal.continuous_at_rpow_const',
 'nnreal.continuous_rpow_const',
 'laurent_measures_ses.nnreal.tsum_geom_arit_inequality',
 'laurent_measures_ses.θ_bound',
 "laurent_measures_ses.θ_bound'",
 'laurent_measures.psi_bound',
 'invpoly.short_exact',
 'laurent_measures.epi_and_is_iso',
 'liquid_tensor_experiment']

[Riccardo Brasca]

Ah, it's done by gephi.

[Riccardo Brasca]

Am I supposed to feed to gephi the file data.yaml? The other one?

[Johan Commelin]

cc @Patrick Massot

[Patrick Massot]

Riccardo, this is explained in the README. You need to use G.write('riccardo.gexf') to get something you can open in gephi

[Riccardo Brasca]

test.png file:///home/ricky/Documenti/test.png

I've played a little bit with gephi, and the graph looks like this

[Riccardo Brasca]

The big node in the middle is docs#id_tag, that makes sense I guess..

[Riccardo Brasca]

Tomorrow I will remove the nodes in core.

[Kevin Buzzard]

@Riccardo Brasca are you going to tweet it?

[Adam Topaz]

It would be nice to include the text saying what each of the (main) colours mean.

[Riccardo Brasca]

I will do a better version later today, then @Kevin Buzzard feel free to tweet it, you have much more followers than me

[Riccardo Brasca]

I am sharing what I did to get the graph, to see if someone has some suggestions to make it more interesting. To get rid of foundational stuff and things in core I did lib.prune_foundations(files=['elan']). Then I used G.component_of('liquid_tensor_experiment') since we probably only want the results used to prove liquid_tensor_experiment.

This graph has 16710 nodes and 270489 edges, with an average degree of 32,375 and a diameter of ... wait for it.

Modularity found 9 classes. Here are some results in each class.

This is definitely category theory.

category_theory.limits.is_zero_initial  lemma   0
category_theory.limits.equalizer.ι  definition  0
category_theory.limits.colimit.desc definition  0

Stuff related to multiset

list.find_cons_of_pos   lemma   1
multiset.ndinter_le_right   lemma   1
multiset.fold   definition  1

Topology?

continuous_linear_map.lipschitz lemma   2
nnreal.topological_semiring instance    2
CLCFPTinv₂.res_refl lemma   2
pseudo_normed_group.injective_cast_le   lemma   2
laurent_measures.shift_add_monoid_hom_apply_to_fun  lemma   2
hom_complex_QprimeFP_nat_iso_aux_system_naturality_in_T_inv lemma   2

This is less clear, maybe analysis.

metric.bounded.union    lemma   3
cau_seq.lim_eq_of_equiv_const   lemma   3
one_div_neg_one_eq_neg_one  lemma   3
sub_mul lemma   3
rat.cast_inv    lemma   3
real.exp_bound_div_one_sub_of_interval_approx   lemma   3
pow_unbounded_of_one_lt lemma   3

Basic algebra.

finsupp.single_mem_supported    lemma   4
add_monoid_hom.lift_of_surjective_apply lemma   4
submodule.fg    definition  4
linear_equiv.linear_map.has_coe instance    4
continuous_linear_map.has_sub   instance    4
polynomial.degree_neg   lemma   4
finset.smul_sum lemma   4
add_monoid_hom.pushout_inl  definition  4
add_equiv.of_bijective  definition  4

Cardinal and friends.

cardinal.mk_fintype lemma   5
ordinal.one_add_of_omega_le lemma   5
cardinal.lift_one   lemma   5
rel_embedding   structure   5

Again category theory! I don't know why, we can maybe use the same color.

homological_complex.exact.congr lemma   6
category_theory.strong_mono_category    class   6
category_theory.triangulated.pretriangulated    class   6
category_theory.arrow.lift_mk'_left lemma   6

I don't know what this is, but it is very small (only 25 nodes)

not_covby_iff   lemma   7
order.covby_succ    lemma   7
order.lt_succ_iff_not_is_max    lemma   7
order.le_of_lt_succ lemma   7
order.succ_le_of_lt lemma   7
wcovby.covby_of_lt  lemma   7

Topology again?

embedding.is_compact_iff_is_compact_image   lemma   8
filter.prod_comm    lemma   8
ne_top_of_lt    lemma   8
is_irreducible.is_connected lemma   8
is_open.add_left    lemma   8
interior_eq_nhds'   lemma   8

[Riccardo Brasca]

/poll <Where liquid_tensor_experiment is?>
0
1
2
3
4
5
6
7
8

[Yaël Dillies]

The very small stuff with 25 nodes is the order theory I've been doing!

[Johan Commelin]

Maybe number 6 is homological algebra?

[Riccardo Brasca]

Is it normal that first_target is not there?

[Johan Commelin]

It is called thm95.profinite in Lean, I guess.

[Johan Commelin]

https://github.com/leanprover-community/lean-liquid//blob/b646a1f131d272c7d994abeff318e626561a666e/src/liquid.lean#L101

[Johan Commelin]

thm94

[Johan Commelin]

first_target is the LaTeX label in the blueprint

[Riccardo Brasca]

https://github.com/leanprover-community/lean-liquid/blob/0a3c7ec2eb620a158e775233c47ad217127b5281/src/liquid.lean#L37

:thinking:

[Riccardo Brasca]

In any case the only thm94 that is there is thm94.explicit

[Johan Commelin]

Ooh, lol. I forgot about that one :oops: :see_no_evil:

[Johan Commelin]

thm94.explicit is used in Lbar/ext.lean.

[Johan Commelin]

https://github.com/leanprover-community/lean-liquid/blob/0a3c7ec2eb620a158e775233c47ad217127b5281/src/thm95/default.lean#L158

[Riccardo Brasca]

I mean that if we delete thm94 then liquid_tensor_experiment should still compile, unless I messed up something.

[Johan Commelin]

Yes, technically we can delete all of liquid.lean

[Johan Commelin]

We only need thm94.explicit from the file thm95/default.lean (yes, I know, the names are confusing).

[Johan Commelin]

Although

src/Lbar/ext_preamble.lean
2:import liquid

will cause breakage if we actually do that.

[Riccardo Brasca]

LTE.png file:///home/ricky/lean/lean-liquid/LTE.png

If we like this image I can add the labels. I don't know how to avoid the drift in the bottom without having a too dense image.

[Riccardo Brasca]

LTE_labels.png
@Kevin Buzzard feel free to tweet it. I can change the labels, but I don't think I am able to make it nicer

[Kevin Buzzard]

What have "cardinals" got to do with things? Did they really play a role? Can we think of a better label?

[Kevin Buzzard]

How about "finiteness"?

[Eric Wieser]

How viable would it be to generate another version of the graph with everything from mathlib at 50% opacity? My thinking was this would styll show both LTE is a substantial body of work, but also that mathlib was essential in providing foundations for it.

[Riccardo Brasca]

Cardinals were there even in the first part of the project

[Riccardo Brasca]

https://leanprover.zulipchat.com/#narrow/stream/267928-condensed-mathematics/topic/Actual.20graph/near/242346884

[Kevin Buzzard]

What I don't like is that the graph right now seems to say "an obscure mathematical concept was important in about 10% of the results" which I think is misleading (and unhelpful).

[Riccardo Brasca]

Eric Wieser said:

How viable would it be to generate another version of the graph with everything from mathlib at 50% opacity? My thinking was this would styll show both LTE is a substantial body of work, but also that mathlib was essential in providing foundations for it.

Unfortunately I have no idea how to do this.

[Eric Wieser]

I think you'd have to add an "ismathlib" flag to the graph on these lines:

https://github.com/leanprover-community/leancrawler/blob/3d5dc53e40636f106be37c67e6af84109d888679/leancrawler/crawler.py#L270-L273

which would at least ensure that data makes it to the .gexf

[Riccardo Brasca]

Kevin Buzzard said:

What I don't like is that the graph right now seems to say "an obscure mathematical concept was important in about 10% of the results" which I think is misleading (and unhelpful).

I agree this looks strange, but if you look at the results we used it really seems that the only reasonable label is "cardinal" or "ordinal". Here is a random selection.

ordinal.nat_lt_card
subrel.rel_embedding
nat.add_succ_sub_one
cardinal.mk_prod
ordinal.card_zero
cardinal.omega_mul_mk_eq
ordinal.succ
ordinal.has_add
cardinal.sum_const'
cardinal.mk_Prop
ordinal.enum_lt_enum
order_iso.symm_apply_apply
ordinal.lift_lt
rel_embedding.map_rel_iff
ordinal.lsub_le_iff
ordinal.nat_lt_omega
ordinal.enum_typein
cardinal.omega_le_mk
cardinal.zero_mul
cardinal.lift_le
ordinal.lift_add
cardinal.lift_lt
cardinal.power
ordinal.lift_down'
covariant_swap_mul_le_of_covariant_mul_le
initial_seg.unique_of_extensional
cardinal.ord_nat
cardinal.mk_vector
ordinal.sub_nonempty
empty_relation.is_well_order
cardinal.has_add
ordinal.lt_sub
cardinal.mk_le_mk_of_subset
strict_mono.compares
cardinal.mk_pi
cardinal.power_one
fin.succ_above_pred
ordinal.lt_lsub_iff
strict_mono.order_iso
ordinal.omega_is_limit
order_iso.to_order_embedding
order_iso.symm_apply_le
ordinal.lift
ordinal.add_le_of_limit
ordinal.has_lt
ordinal.typein_lt_type
fin.exists_succ_above_eq
ordinal.type_lt
ordinal.card_typein
fin.succ_above_eq_zero_iff
is_order_connected_of_is_strict_total_order'
ordinal.lift_one
ordinal.infinite_pigeonhole
is_well_order.is_irrefl
is_extensional_of_is_strict_total_order'
le_of_forall_lt
fin.coe_zero
cardinal.lift_mk_eq
cardinal.one_lt_omega
strict_order.cof
principal_seg.has_coe_initial_seg
order_iso.trans
order_hom_class
initial_seg.init_iff
cardinal.lift_sup
cardinal.sum
cardinal.induction_on₃
order_iso.symm
cardinal.lift_add
well_founded.min
ordinal.zero_or_succ_or_limit

[Kevin Buzzard]

Are the cardinals in practice all finite?

[Riccardo Brasca]

I don't know, but I suspect they're at most countable.

[Kevin Buzzard]

Can you relabel it "finiteness" then?

[Riccardo Brasca]

Oh, I didn't save the gimp file... give me 10 minutes

[Riccardo Brasca]

LTE_labels.png
Voilà

[Riccardo Brasca]

Eric Wieser said:

I think you'd have to add an "ismathlib" flag to the graph on these lines:

https://github.com/leanprover-community/leancrawler/blob/3d5dc53e40636f106be37c67e6af84109d888679/leancrawler/crawler.py#L270-L273

which would at least ensure that data makes it to the .gexf

Yes, the problem is how to find mathlib declaration. Once this is done gephi can handle the opacity. I agree it can be done, but I basically don't know any python...

[Eric Wieser]

A quick implementation would probably be

graph.nodes[name]['is_mathlib'] = "/mathlib/" in item.filename

[Violeta Hernández]

Kevin Buzzard said:

What I don't like is that the graph right now seems to say "an obscure mathematical concept was important in about 10% of the results" which I think is misleading (and unhelpful).

Cardinals are obscure? I think a more precise statement would be "they prove a bunch of weird foundational results and that's it" :stuck_out_tongue:

[Johan Commelin]

Can confirm that cardinals are pretty obscure.

[Riccardo Brasca]

Eric Wieser said:

A quick implementation would probably be

graph.nodes[name]['is_mathlib'] = "/mathlib/" in item.filename

I've added this line to the source code but nothing has changed.

[Riccardo Brasca]

Sorry, it worked perfectly!

[Riccardo Brasca]

graph.gephi

Here is the gephi file. It should be easy to set opacity of the note with is_mathlib, but for some reason the setting is ignored when I change it (I can change the color of a single node, but that's it).

[Kevin Buzzard]

What percentage of the nodes are core Lean?

[Riccardo Brasca]

I've removed everything from core (at least, I think I did) to avoid having a gigantic node corresponding to docs#id_tag and similar stuff

[Riccardo Brasca]

Including core there are 17381 nodes, so only 671 are in core. I don't know, maybe it was a better idea to keep them, now nat is not there.

Note that in any case I used the prune_foundations function to avoid the definition of eq and stuff like that. Without removing anything there are 19538 nodes. The biggest one is eq, with a degree of 9902.

[Eric Wieser]

Riccardo Brasca said:

graph.gephi

Here is the gephi file. It should be easy to set opacity of the note with is_mathlib, but for some reason the setting is ignored when I change it (I can change the color of a single node, but that's it).

I'm afraid I have no experience at all with (nor installation of!) gephi