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.
5
questions
1
vote
1
answer
209
views
Prove an upper bound on the computation time of the Euclidean algorithm in lean4
I've heard that proof assistants like lean4 can formalize all the usual math.
I'm interested to see how they formalize the complexity estimates of algorithms, since they are not often discussed ...
- 171
6
votes
3
answers
322
views
What proof assistants can reason about the complexity of its *own* programs?
This is obviously a question inspired by can proof assistants reason about the complexity of programs?.
Here, the question involves a degree of meta-programming (or reflection if you'd prefer).
For ...
- 429
11
votes
3
answers
763
views
can proof assistants reason about complexity of programs?
Sorry if this question is too basic or vague, I'm new to using proof assistants.
Using a proof assistant, one can construct the type Ordered n t of ordered lists of ...
- 213
2
votes
1
answer
246
views
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 ...
- 9,195
8
votes
2
answers
221
views
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 ...
- 2,220