-
Notifications
You must be signed in to change notification settings - Fork 40
Commit
This PR: **1.** Adds 4 more cancellative magmas that were found through hand-guided search and which refute 31 of the 29688 implications still open after #281, bringing down the number to 29657. The idea was to find for cancellative magmas that specifically fail to satisfy large one-variable laws. The addition of the new magmas also results in a slightly better plan (with fewer Lean checks required). **2.** Re-runs the transitive closure pruning using the large number of recently proved implications. This further pushes down the number of explicitly proven implications from 604701 to 581162 . **3.** Adds a minor QoL improvement to variable counting in `finite_magma_tools`, which makes it more useful for #278 -style experimentation.
- Loading branch information
There are no files selected for viewing
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.
Some generated files are not rendered by default. Learn more about how customized files appear on GitHub.