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

DATA: Add Equation5105, Equation28393 and Equation374794 to the All4x4Tables #375

Open
Command-Master opened this issue Oct 6, 2024 · 3 comments

Comments

@Command-Master
Copy link
Contributor

Command-Master commented Oct 6, 2024

Currently a large number of our unknown implications are simply ones involving Equation5105, Equation28393 and Equation374794, as most automated tools ignore them. Since none of them hold for non-trivial finite magmas, one direction should be easily resolvable simply by adding them to some lists of Facts in All4x4Tables's refutations.
The other direction will probably be quite hard, as Equation5105 -> Equation2 is open (see https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Equation.205105.20-.3E.20Equation.202 on Zulip).

@Command-Master
Copy link
Contributor Author

Pinging @zaklogician

@teorth
Copy link
Owner

teorth commented Oct 6, 2024

This could be automated if #142 was implemented.

@zaklogician
Copy link
Contributor

Linking this to #725

The current finite_magma_tools assume that the equations are numbered according to their line number in equations.txt.

This won't be tenable for Equation374794 -- we don't want to deal with a 375k line text file. So resolving this would require refactoring there. But then it makes sense to resolve it in one go as part of 725.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
Status: Unclaimed Outstanding Tasks
Development

No branches or pull requests

4 participants