A webpage to view equations

Stream: Equational

[Nicholas Carlini]

I started working on equational#209 to help look at equations. I've sent a PR on equational#223, but:

1. It would require committing 5MB of javascript to import the whole 4694^2 pairs, which is a lot. I don't know the best way to deal with this. (Have lake build generate it for everyone? Some other option?)
2. It's kind of clunky and slow, because of the whole 4696^2 thing. I'm going to precompute the pages so it'll load faster in the next commit.
3. I don't know if it does what people would want it to. Please let me know if anyone wants a feature out of it that's not there now. <- this is the important one

If you don't want to clone my PR and get a copy locally, I'm temporarily hosting it here

[Daniel Weber]

If you compress the relations it should only be about 7.5MB

[Daniel Weber]

If we can get an SQL server storing this data that'd probably be the best

[Nicholas Carlini]

It's already compressed to 5MB and---if you want to be really ugly---I can actually compress it to 500k by pretending it's a PNG. The 2d structure lets PNG compress a lot better even though this is a dirty awful hack.

[Daniel Weber]

Oh, sorry, I read 50MB

[Nicholas Carlini]

(I was trying to keep it a single html file just so people who want to look at it don't have to start up some crazy backend framework just to view things.)

[Daniel Weber]

You should merge main and rerun it, by the way, as there's a bug in equational#206 which created false conjectures

[Nicholas Carlini]

Yeah I'm the one who found the bug when preparing for this UI

[Daniel Weber]

Nicholas Carlini said:

(I was trying to keep it a single html file just so people who want to look at it don't have to start up some crazy backend framework just to view things.)

I think ideally this should appear on the project page, not require people to run it themselves

[Daniel Weber]

Nicholas Carlini said:

Yeah I'm the one who found the bug when preparing for this UI

Oh, right, sorry. I reverted it, so now there should be no contradictions

[Nicholas Carlini]

Yeah, but even there having it a single html file with no backend is convenient for hosting too

[Amir Livne Bar-on]

If you go by equivalence class there'll be 4 times less data, right? But that will necessitate adding another page, showing the proofs forming each class.

[Terence Tao]

For the implications, one can store just the irreducible implications: of the form EquationX => EquationY where there is no inequivalent EquationZ such that EquationX => EquationZ => EquationY. The full list of implications from a given starting point can then be easily obtained by iteration.

For the anti-implications, there isn't really a comparable trick, but if one only stores the unknown implications, one can recover the anti-implications from the iterated implications and the unknown implications by set operations. Since the unknown implications is already down to like 10% of the total, this should be a significant savings in data size.

[Daniel Weber]

There is a similar trick for anti-implications. Constructing a graph on two copies of the set of equations, and for each implication a -> b adding copy1(b) -> copy1(a), copy2(b) -> copy2(a) and for each anti-implication ¬ (a -> b) adding copy1(a) -> copy2(b), the transitive closure is exactly what's known implicitly (this is also how Closure.lean works), so we can compute the transitive reduction of this graph

[Amir Livne Bar-on]

Or your trick with the vertices for specific magmas, that also works quite well, and is more compact for our data

[Zoltan A. Kocsis (Z.A.K.)]

Possible bug note: in the temporary hosted version, entering x = x and pressing the Jump to Equation button takes me to the equation details for ## Equation2[x = y].

[Nicholas Carlini]

Zoltan A. Kocsis (Z.A.K.) said:

Possible bug note: in the temporary hosted version, entering x = x and pressing the Jump to Equation button takes me to the equation details for ## Equation2[x = y].

Hah, off-by-one

[Sebastian Luther]

The web site is really interesting, but I'm wondering if the data is correct. I'm looking at Equation467 with "Show only explicit proofs". It lists several in the "This equation implies (=>)" column, but I can't find most of them. And I think most of them are not correct.

[Nicholas Carlini]

This is entirely possible, I was having trouble with extract_implications outcomes previously and it's possibly still messed up. I'll take a look

[Nicholas Carlini]

The webpage is certainly wrong. It says x=x implies x=y which ... no. I don't think I've just inverted it either. Will need to investigate to see if it's the data or my processing of the data

[Joachim Breitner]

Nicholas Carlini said:

It's already compressed to 5MB and---if you want to be really ugly---I can actually compress it to 500k by pretending it's a PNG. The 2d structure lets PNG compress a lot better even though this is a dirty awful hack.

I don't think storing inherently 2d data as an image is a horrible hack. At most it is a cute hack.

[Nicholas Carlini]

Sebastian Luther said:

The web site is really interesting, but I'm wondering if the data is correct. I'm looking at Equation467 with "Show only explicit proofs". It lists several in the "This equation implies (=>)" column, but I can't find most of them. And I think most of them are not correct.

Okay I've fixed it. I got the equation numbering wrong (again). Updated this live version.

[Joachim Breitner]

This is super useful. At the hike today I wondered “For the associativity law, surely we can easily decide all outgoing edges”, and the web page quickly showed me that this low-hanging fruit has been plucked already

[Sebastian Luther]

Nicholas Carlini schrieb:

Sebastian Luther said:

The web site is really interesting, but I'm wondering if the data is correct. I'm looking at Equation467 with "Show only explicit proofs". It lists several in the "This equation implies (=>)" column, but I can't find most of them. And I think most of them are not correct.

Okay I've fixed it. I got the equation numbering wrong (again). Updated this live version.

I think the data for Equation467 is still wrong.

[Nicholas Carlini]

Can you give me an example of the implications thats wrong?

[Sebastian Luther]

Nicholas Carlini schrieb:

Can you give me an example of the implications thats wrong?

15

[Nicholas Carlini]

Equation467 =/> Equation15 is wrong or Equation 15 => Equation467?

[Joachim Breitner]

Joachim Breitner said:

This is super useful. At the hike today I wondered “For the associativity law, surely we can easily decide all outgoing edges”, and the web page quickly showed me that this low-hanging fruit has been plucked already

Although now I am confused. I searched for x ∘ (y ∘ z) = (x ∘ y) ∘ z but it shows me Equation4513[x ∘ (y ∘ z) = (x ∘ y) ∘ w]. Off by one error somewhere?

[Nicholas Carlini]

Oops fixed that lookup function

[Sebastian Luther]

Nicholas Carlini schrieb:

Equation467 =/> Equation15 is wrong or Equation 15 => Equation467?

The "This equation implies (=>):" list says that Equation467 implies Equation15, but this is not true.
What is true is that Equation467 implies Equation411, but this one is missing from the "This equation implies (=>)" list.

[Joachim Breitner]

Nicholas Carlini said:

Oops fixed that lookup function

Thanks! Would be good to have the equation in the url hash somehow, for easier linking/navigation.

[Nicholas Carlini]

Sebastian Luther said:

Nicholas Carlini schrieb:

Equation467 =/> Equation15 is wrong or Equation 15 => Equation467?

The "This equation implies (=>):" list says that Equation467 implies Equation15, but this is not true.
What is true is that Equation467 implies Equation411, but this one is missing from the "This equation implies (=>)" list.

Sorry, are you seeing something different than me? Screenshot 2024-10-03 at 10.10.35.png

[Nicholas Carlini]

Joachim Breitner said:

Nicholas Carlini said:

Oops fixed that lookup function

Thanks! Would be good to have the equation in the url hash somehow, for easier linking/navigation.

Can do.

[Sebastian Luther]

Nicholas Carlini schrieb:

Sebastian Luther said:

Nicholas Carlini schrieb:

Equation467 =/> Equation15 is wrong or Equation 15 => Equation467?

The "This equation implies (=>):" list says that Equation467 implies Equation15, but this is not true.
What is true is that Equation467 implies Equation411, but this one is missing from the "This equation implies (=>)" list.

Sorry, are you seeing something different than me? Screenshot 2024-10-03 at 10.10.35.png

Yes.
grafik.png

[Nicholas Carlini]

Oh is this on your local version?

[Nicholas Carlini]

Oh no it's live. Can you force refresh the page?

[Nicholas Carlini]

Your browser may be caching the old javascript file

[Sebastian Luther]

Nicholas Carlini schrieb:

Oh is this on your local version?

Yes, that fixed it.

[Zoltan A. Kocsis (Z.A.K.)]

If you have<script src="out.js?v=SOME_RANDOM_NUMBER"> and change the number when you update the live page to a new release, that should prevent browsers from serving up old cached copies.

[Nicholas Carlini]

Yeah. I just pushed a change adding just a ? at the end a few minutes ago. Will do this for the rest once I find a way to shrink the implication set.

[Sebastian Luther]

What data format does the page use? I see this large array in the js file. What do you think about making it a bit more explicit what the numbers mean? People could then download the data for their tools without fiddling with lean.

[Nicholas Carlini]

You can get the same data from extract_implications which is where I get it. It's a little tricky to get right though, or I had a somewhat hard time, I can try to document that a bit more.The javascript file is RLE compressed to save space and I'd rather keep it this way (or probably even more compressed)

[Sebastian Luther]

It wouldn't have to be the same file. The page could use the compressed version and the more readable version could be an extra download.

[Nicholas Carlini]

Yeah -- I guess my comment is this is already something you can get by running the extract_implications lean file

[Sebastian Luther]

I tried some days ago and couldn't get it to work. Still getting the same error:
$ lake exe extract_implications
uncaught exception: object file '././.lake/build/lib/equational_theories.olean' of module equational_theories does not exist

[Nicholas Carlini]

I also got some crashes in this and don't fully undestand how to run it properly. (I had to delete a file even after a clean install.) This could be worth bringing up separately to get good documentation here

[Amir Livne Bar-on]

Re format, in CSV it's clearer what each cell means. If we choose a single-char mnemonic for each outcome it's 43 MB, and gzipped (which the server probably does automatically?) it's 470 KB

[Terence Tao]

Great tool! I am going to try to play with it some. A surprisingly large number of equations are now "complete" in that there are no unknown consequences of that equation. In particular some of my task requests have already been completed and can be retired!

Feature request: is it possible to list an equation in boldface if it appears in Equations.lean instead of AllEquations.lean?

[Nicholas Carlini]

Terence Tao said:

Feature request: is it possible to list an equation in boldface if it appears in Equations.lean instead of AllEquations.lean?

Done. Working on a change to hide equivalences now.

[Terence Tao]

It seems the boldfacing is not yet activated on the "This equation is implied by" columns.

[Terence Tao]

Another feature request (lower priority): make the equations listed in the various implications clickable to their own implication page, thus allowing one to "walk" through the implication graph

[Nicholas Carlini]

I've updated the UI and will start preparing a PR with a simple script that can be used to generate the .js file. Changes:

• You can hide/show equivalences
• Fixed the bolding for all Equations.lean
• And you can now click through each of the equations
• Updated the operator to the new one. The "equation finder" still uses * because it's easy to type.

I do not understand the CI thing well enough yet to know if the webpage can contain files that are generated by the CI but are not contained in the repository so that we don't have to rewrite this big file each time an implication changes. I will look into that because that would be the best case

[David Renshaw]

At CI time you can generate files and put them under the home_page/ directory and jekyll will pick them up

[Nicholas Carlini]

Oh fantastic. I will go figure out how to do that

[Nicholas Carlini]

(Importantly, this won't cause them to be committed but will be visible, right?)

[David Renshaw]

at least any .md will be converted to an html

[David Renshaw]

and probably any file in assets gets put on the site

[David Renshaw]

to get a local setup, I installed ruby via rbenv, installed the gems via bundler, and then served the site via jekyll serve --watch

[Terence Tao]

A "bug": currently Equation2 is listed as implying and implied by Equation6, separately to also being listed as equivalent. (None of the statements are incorrect, but some are redundant.)

OK, I think basically the code thinks that Equation6, which for some reason is the designated driver of Equation2's equivalence class, is distinct enough from Equation2 that it gets to go in the "implies" and "implied by" columns. If one explicitly excludes equivalent classes from those columns it should be ok.

[Nicholas Carlini]

Got distracted working on another PR, but will return to adding this to the CI tomorrow. In the meantime I've updated the tmp page to fix that bug

[Terence Tao]

Another small feature request: add a way to jump from an equation to its dual, using for instance the link at https://github.com/teorth/equational_theories/blob/main/data/dual_equations.md or the script at https://github.com/teorth/equational_theories/blob/main/scripts/find_dual.py to generate the duality relation

[Terence Tao]

Another feature request: have the URL have the ability to accept as input an equation number, so that one can provide URLs that link directly to the page for a single equation, rather than to the full list of implications.

[Nicholas Carlini]

Okay both of these are done. Equation linking:
https://nicholas.carlini.com/tmp/view.html?234

I'm now starting writing the code necessary to hook this up to the CI to make a permanent version.

[Terence Tao]

A preliminary version is now up at https://teorth.github.io/equational_theories/implications/ . I love the very small numbers on the last two columns. Hopefully it can be debugged (especially with regards to the CI) and linked up to the main page soon!

[Nicholas Carlini]

I believe it's working with the CI now. Given that it's running here that means in principle everything went through properly

[Terence Tao]

By the way, clicking "back" on the browser from an equation page produces a popup with a message like "pophttps://teorth.github.io/equational_theories/implications/view.html?3", instead of going back to the main page.

[Nicholas Carlini]

Oops. Debug code stayed in...

[Pietro Monticone]

It would probably be a bit better to have the table header remain fixed while scrolling down the content.

[Terence Tao]

The boldfacing of Equations.lean equations seems no longer in effect. Also I don't see the web page implementing equational#325 yet but perhaps that is just a temporary lag.

[Nicholas Carlini]

It looks like the CI build was canceled (or timed out?)
Screenshot 2024-10-05 at 11.27.07.png

[David Renshaw]

that happens when another commit lands before your commit's CI has time to finish

[David Renshaw]

I love the "prove this!" link.

[Nicholas Carlini]

Terence Tao said:

The boldfacing of Equations.lean equations seems no longer in effect.

Looks like Equations.lean changed and my parsing of it is not very robust. Fixed in equational#328

[Pietro Monticone]

(deleted)

[Pietro Monticone]

Pietro Monticone said:

It would probably be a bit better to have the table header remain fixed while scrolling down the content.

Done https://teorth.github.io/equational_theories/implications/

[Terence Tao]

Another request is to have a timestamp of when the graph was retrieved (I assume it is not 100% real time, so having this information may help reduce confusion on this point).

[Nicholas Carlini]

equational#339

[Terence Tao]

One more minor request: some feature to export the implication graph to some easily machine-readable format (e.g., JSON) for third parties to work with. (This file could just be kept in some static location in the repository, and updated with each CI.)

[Nicholas Carlini]

This is basically already done. I can just expose it in another file.

Do you care about whether or not a statement is proven explicitly/implicitly, and proven/conjectured? The current internal datastructure stores this, but if it's not interesting, it may be easier for people to parse if it's just yes/no/unknown.

[Terence Tao]

One could perhaps have two files, one in which one just records true/false/unknown, and one which has the implicit/explicit and proven/conjectured metadata. It is a little bit important right now because technically we don't have full lean proofs of implicit implications. They should not be too hard to autogenerate from the data that we already have, but we haven't gotten around to doing that.

A related feature to implement at some point (but not urgently) is to have the ability to click on an implicitly proven statement and see the chain of explicit statements that imply it. Presumably all the graph reduction scripts can be retooled to provide this sort of output as an additional option.

[David Renshaw]

some touchups for the "Prove This!" link: equational#376