All Questions
Tagged with soft-question proof-search
1
question
-3
votes
1
answer
150
views
Could we speed up ATP or ATD using a directed graph that appears to work like a gigantic brain?
So I'm not sure how things are done in Lean4 or Coq, but I'm interested in their search features. For example, "Search for all theorems that get satisfied given a user-defined list of ...
