search

teorth / equational_theories

A project to map out the relations between different equational theories of Magmas.
https://teorth.github.io/equational_theories/
Apache License 2.0
198 stars 50 forks source link

FRONTEND: Generate a list of "Vampire-hard" implications as a challenge, with each implication linked to a Lean playground to prove them #370

Open teorth opened 3 weeks ago

teorth commented 3 weeks ago

Discussed at https://leanprover.zulipchat.com/#narrow/stream/458659-Equational/topic/Is.20it.20plausable.20that.20all.20remaining.20implications.20are.20false.3F . Generation of lean playground versions of implications is already implemented in #316.

This challenge can be linked to from the README.md page. The list of Vampire-hard implications might need to be updated over time as new implications (not covered by previous Vampire runs) trickle in (and perhaps we may end up using a different measure of hardness than Vampire run time).

One can also do this for anti-implications that Vampire can establish by saturation methods without producing a finite model.

A more sophisticated version of this would be to serve up a random problem at a specified "Vampire difficulty level".

Command-Master commented 3 weeks ago

Are these supposed to be unknown implications as ways to manually contribute to the project, or hard (but known) implications to prove as a challenge/game?

teorth commented 3 weeks ago

I guess one could serve up both types as part of the difficulty level setting (so "Unknown" is the hardest difficulty level).

Command-Master commented 3 weeks ago

I think Vampire run time is too coarse to meaningfully distinguish between implications, perhaps the number of proof steps it takes?