New data – new pictures?

Stream: Equational

[Joachim Breitner]

I’m excited to see a picture that includes all new implications and anti-implications. I lost track of who is generating pictures how – is there already a picture generation script that works with the output of extract_implications, maybe even with support for the new facts format for antiimplication?

[Vlad Tsyrklevich]

cc @Andrii Kurdiumov Just looked at the tool, doesn't look like it supports parsing the new form of data for anti-implications

[Vlad Tsyrklevich]

Speaking of which, I should submit the script to generate implication graphs

[Terence Tao]

Is there a plain text file listing all the implications and anti-implications obtained thus far? I am already recieving inquiries from new people wanting to create some visualizations and it would be nice to have a text file that one could simply give them, even if it is not actively updated as new submissions come in.

[Daniel Weber]

direct.tar.xz these are the direct implications/nonimplications
closure.tar.xz and this is the transitive closure

[Terence Tao]

Are there some statistics on how many direct and transitive relations have been obtained so far, and how many remain? I am thinking of posting these stats together with the data sets on the README.md as part of the ongoing progress.

[Andrii Kurdiumov]

It was approximately 4.5m direct relations. Out of ~24M or so.

[Andrii Kurdiumov]

I have to run with latest files which sent here to give you explicit number.

[Terence Tao]

Eventually it will be nice to have an automated scheduled update of these stats eg on a daily basis to form a time series

[Andrii Kurdiumov]

That’s doable.

[Andrii Kurdiumov]

When it should be displayed? On the GitHub only, or in blueprint too?

[Daniel Weber]

In terms of equational#29 the current counts are:
implicit_proof_false: 12764328
implicit_proof_true: 4494090
unknown: 4014155
explicit_proof_false: 739207
explicit_proof_true: 21791
implicit_conjecture_true: 64
explicit_conjecture_true: 1

[Amir Livne Bar-on]

(deleted)

[Amir Livne Bar-on]

Terence Tao said:

Is there a plain text file listing all the implications and anti-implications obtained thus far? I am already recieving inquiries from new people wanting to create some visualizations and it would be nice to have a text file that one could simply give them, even if it is not actively updated as new submissions come in.

We can add this to CI: the extract_implications Lean program generates a simple compact format, we can host the results on the web site

[Terence Tao]

How does this square with the claim of 4.5 direct relations?

[Andrii Kurdiumov]

Oops. I may have to distinguish direct relationship and these which are transitive closure of these direct relationships.

[Terence Tao]

OK then the numbers roughly make sense

[Andrii Kurdiumov]

4.5m was from latter. And that from directly Lean files. Not a new format which I have to add.

[Terence Tao]

Anyway the upshot is that we have resolved about 80% of the implications so far. Of course that was the lowest hanging fruit, I expect the going to be slower now. (Though I have just received word that there are going to be some sizeable AI-assisted contributions coming down the pipeline shortly...)

[Daniel Weber]

There also hasn't been any large execution of SMT solvers yet, right?

[Andrii Kurdiumov]

About pictures. Does script which generates SVG is in the repo?

[Terence Tao]

Andrii Kurdiumov said:

When it should be displayed? On the GitHub only, or in blueprint too?

I think Github is fine for now. I'll open a task for this. (I assume that equational#126 and hence equational#29 is close to completed for now.)

[Terence Tao]

Daniel Weber said:

There also hasn't been any large execution of SMT solvers yet, right?

There is this blog post at https://www.philipzucker.com/ruler/ but I can't determine exactly whether there was an actual large scale data run here or just a proof of concept

[Daniel Weber]

I think it's ready to be merged now, yes. I now added code to compute these counts, which can be run using lake exe extract_implications outcomes --hist <files>

[Amir Livne Bar-on]

Another count that might be interesting is unknown, modulo equivalences. That is, if we know A=>B and B=>A, then count X=>A and X=>B as one unknown (and also in the opposite direction). This comes out to 3182453

[Terence Tao]

Nice, so now only 15% or so of the original total. Is it easy currently to create a text file of these 3182453 equivalences (e.g., replacing each equation with the lowest numbered equation known to be equivalent)? One could imagine it could help a large SMT or AI run if they could just feed in such a file instead of the original 22m.

[Nicholas Carlini]

Seconded that I would find such a list very useful, especially if it could be kept (mostly) up to date automatically.

[Vlad Tsyrklevich]

Andrii Kurdiumov said:

About pictures. Does script which generates SVG is in the repo?

The implication graph, or something else?

[Nicholas Carlini]

It might also be fun to have a graph showing the number of remaining equations as a function over time, to see how things are progressing.

[Andrii Kurdiumov]

@Vlad Tsyrklevich yes, implictions.svg, I think they are interesting perspective, even if very large.

[Vlad Tsyrklevich]

See https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Some.20more.20implication.20visualizations/near/473883222 I will submit the script today

[Terence Tao]

Created equational#171 and equational#173 to request these statistics on a continuing basis. Actually just having a one-shot generated file of reduced outstanding implications would be useful for people to run all sorts of other algorithms on it. For instance, each of the metatheorems in https://teorth.github.io/equational_theories/blueprint/sect0002.html could be run against that list.

EDIT: I see that Amir has this separately at https://github.com/amirlb/equational_theories/tree/unknown-implications . I've modified equational#173 to request integrating this into the main repo.