The 'extra' equations

Stream: Equational

[Alex Meiburg]

Since the project's wrapping up, I was wondering what will properly become of the "extra" equations we have listed at Basic.lean and this wiki page. (Note: each of those lists has some equations the others don't.)

Given that these equations had some special extra interest, I had hoped that they would also be put into the graph of equations. Some are "known" to be hard like 5093, but I'm optimistic that most could be rapidly dispatched and placed snugly in the graph. I know that all this tooling exists to find non-/implications ... but I've had trouble running almost any of it myself.

Would someone, maybe, be so kind as to try running vampire or a countermodel search to try to knock some out? :) Some are already in the repo, e.g. here.

I guess it would also be very cool if they could be added to the equation explorer, but I understand if people don't want the scope creep there.

[Alex Meiburg]

I guess I intend to make a PR to bring {the extra equations on the blueprint, the extra equations in Lean, the wiki page} into agreement as much as possible.

[Terence Tao]

As long as none of the core functionality breaks (eg the dashboard doesnt change, or the main data sets) there shouldnt be any harm in additions to the repo. I guess it could be an excuse to catalogue our general tools and make sure they are documented enough to use for amy future expansion of the project.

[Bruno Le Floch]

It would be useful to have someone summarize how the equation explorer is used by other tools, so what may break if someone changes the code here. There are a bunch of interrelated Github issues, which may need to be sorted into fewer issues to limit duplicate effort.

• EQUATION_EXPLORER: Give an option in equation explorer to allow the "expanded" list of equations beyond the original 4694 #378
• EQUATION EXPLORER: Allow searching/displaying any equation #848
• Update scripts to use Bruno's equation numbering code #1083
• FRONTEND: Get equation explorer to mention canonically equivalent form #1218
• Some equations have names (e.g., left projection, commutative law, NAP, ...), and it may be good for the equation explorer to display those names in the lists of equations implied by and implying the displayed equation.
• Vlad had a list of equations of order 5 equivalent to Equation 2.
• How to deal with large families of known equivalences of higher equations, see a question I posed at #Equational > Questions for equation commentaries @ 💬. A way to deal with that would be to give the Equation Explorer a dictionary {26302:"NaturalCentralGroupoid", 19812:"NaturalCentralGroupoid", ..., 42323216: "HigmanNeumann", ...} and some files HigmanNeumann.md, NaturalCentralGroupoid.md that would be shown for many different high-order equations.

By the way, maybe the equation explorer could document somewhere why some equations are boldfaced (they contain commentary).

EDIT: Just to be clear, I don't plan to touch the equation explorer myself as I don't know enough javascript and web dev in general.

[Emmanuel Osalotioman Osazuwa]

@Bruno Le Floch I created pr [CONTRIBUTIONS] Port Bruno's equation numbering code to ruby. to handle part of issue Update scripts to use Bruno's equation numbering code #1083.
Specifically to port find_equation_id.py to find_equation_id.rb and update generate_graphiti_data.rb to use find_equation_id.rb for generating equation list.

I think issue Update scripts to use Bruno's equation numbering code #1083 can be further broken down into:

• Port Bruno's equation numbering code to JavaScript.

• Port Bruno's equation numbering code to Lean.

• Port Bruno's equation numbering code to Ruby has already been handled by pr [CONTRIBUTIONS] Port Bruno's equation numbering code to ruby. .

More info on the issue could be like files to that require it.

[Shreyas Srinivas]

I am bit under the weather, so I'll get to writing my part tomorrow.