Skip to main content
8 votes

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 ...
Greg Nisbet's user avatar
  • 2,771
7 votes
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 ...
Maximilian Doré's user avatar
5 votes

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 ...
Couchy's user avatar
  • 2,231
5 votes

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, ...
M. Lonardi's user avatar
5 votes
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 ...
Meven Lennon-Bertrand's user avatar
2 votes

Topic for undergraduate thesis

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 ...
Jason Rute's user avatar
  • 8,685
2 votes

Topic for undergraduate thesis

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-...
Andrej Bauer's user avatar
  • 9,154
2 votes
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 ...
Pedro Sánchez Terraf's user avatar
2 votes

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

I'm surprised that the other answer poster Maximilian Doré did not mention their own work Automating Kan composition which is automation for cubical type theories: https://europroofnet.github.io/...
ice1000's user avatar
  • 6,186

Only top scored, non community-wiki answers of a minimum length are eligible