Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

SUBGRAPH: Add the implications/anti-implications between 168 and the other equations as conjecture statements. #35

Closed
teorth opened this issue Sep 28, 2024 · 3 comments

Comments

@teorth
Copy link
Owner

teorth commented Sep 28, 2024

No description provided.

@teorth teorth changed the title SUBGRAPH: Add the implications between 168 and the other equations as proof_wanted statements. SUBGRAPH: Add the implications/anti-implications between 168 and the other equations as proof_wanted statements. Sep 28, 2024
@teorth teorth changed the title SUBGRAPH: Add the implications/anti-implications between 168 and the other equations as proof_wanted statements. SUBGRAPH: Add the implications/anti-implications between 168 and the other equations as conjecture statements. Sep 28, 2024
@few
Copy link
Contributor

few commented Sep 29, 2024

I'm not sure what exactly should happen here. In #103, I have a number of theorems involving equation 168 and others for which a similar issue exists.

@teorth
Copy link
Owner Author

teorth commented Sep 30, 2024

If you already have some implications relating 168 with other Subgraph equations, you can import the relevant Lean file into Subgraph.lean and maybe make a comment within the Subgraph.lean file of the relevant implications that come from imports. (Eventually, our automated tools should be able to work out what all the available implications are from scraping the relevant Lean files, but in any event a human-readable comment is also useful.) Any remaining implications involving 168 that you are unsure of can be left as conjectures (if you have a good guess whether the implication is true or false), or as a comment that the implication is open. You can report all this on this issue and I can then assign further tasks accordingly to resolve the remaining conjectures.

@teorth
Copy link
Owner Author

teorth commented Oct 2, 2024

Closing due to obsolete workflow now that more automated tools are available.

@teorth teorth closed this as completed Oct 2, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
Status: Completed Tasks
Development

No branches or pull requests

2 participants