# Tag Info

### Integration of proof assistants and Wikipedia-like websites?

Metamath has a Proof Explorer; here is one entry. This is mostly a visualization of the proof database set.mm. Because of the nature of the Metamath proof assistant, any new theorems or derived ...
• 2,771
Accepted

### What is the state of the art in proof automation in HoTT/CuTT?

Coq uses type classes to infer h-levels in some simple cases automatically (see Sect. 3.2). Agda does not have an automatic way to manage or infer h-levels. I agree that one has to do quite a bit of ...

### Are search heuristics the main bottleneck for automated theorem provers?

Automated theorem provers rely on the resolution algorithm because it is complete. This means that if a proof exists, the prover is guaranteed to find it. Resolution works as follows: Say you want to ...
• 2,231

### Are search heuristics the main bottleneck for automated theorem provers?

I used to feel the same way. My dream was a computer that would give me the answers I wasn't able to reach because I wasn't smart enough. Now I no longer hope that such a thing is possible; in fact, ...
• 363
Accepted

### Could we speed up ATP or ATD using a directed graph that appears to work like a gigantic brain?

Building that gigantic proof graph as an explicit graph would probably be a very bad idea, given its size and the complexity of "connecting inputs to outputs". Indeed, as you can have an ...
• 5,046

As others have said, your advisor is the best person to discuss this with. Having said that, I think another good place to go is the Lean Zulip. There you can have a back-and-forth discussion (not ...
• 8,685

You profile says you're in applied math, so how about this: Define bipartite graphs as those that have a vertex 2-coloring. Prove that a graph is not bipartite if it has an odd closed walk (a self-...
• 9,154
Accepted

### Semantics verification of an LTL fragment logic

Simp rules for recursive definitions are supposed to be transparent, so you shouldn't need to invoke them for some simple applications. Tools like auto and ...
• 1,003