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
1 vote
1 answer
185 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 ...
Kitamado's user avatar
  • 171
6 votes
3 answers
315 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 ...
Jacques Carette's user avatar
9 votes
3 answers
721 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 ...
Daniel Shapero's user avatar
2 votes
1 answer
228 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 ...
Jason Rute's user avatar
  • 8,135
8 votes
2 answers
210 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 ...
tinlyx's user avatar
  • 1,906