Questions tagged [computational-complexity]

Computational complexity is a measure of the amount of time (computational steps) or space that it takes for an algorithm to solve a particular problem. Use this tag above the complexity of theorem proving algorithms.

Filter by
Sorted by
Tagged with
2 votes
1 answer

Is type checking in "Ideal Lean" computably enumerable?

There are actually two type theoretic foundations of Lean given in Mario Carneiro's master's thesis. They are the same, except for how definitional equality is treated: “algorithmic” definitional ...
  • 5,258
8 votes
2 answers

What is the computational complexity of theorem proving?

I heard theorem proving is a hard problem, hard enough that it contributed to an early AI winter. But how hard? While reading about proof assistants, I have come to realize that there are many types ...
  • 1,412