> "Can a math proof be reached (within a certain number of proof steps) from the axioms?" - equivalent to the halting problem in most practical systems (https:/

> "Can a math proof be reached (within a certain number of proof steps) from the axioms?" - equivalent to the halting problem in most practical systems (https://math.stackexchange.com/questions/3477810/estimating- https://math.stackexchange.com/questions/3477810/estimating-...) The answer that observed this was equivalent to the Halting Problem wasn't keeping the "within a certain number of proof steps" constraint there, but referring to the question of whether an arbitrary proposition was provable or not provable. If you do specify a number of steps in advance, I don't think the problem is solvable faster than brute force in general, but all individual instances can be decided at least by brute force. In fact, there are tactics in computer proof systems where you specify a search depth, and the tactic can tell you whether or not there is a valid proof (using certain rules of inference, which probably won't be all the rules of inference allowed by the system!) closer to your current hypotheses than that depth. This is like the distinction between Gödel's last two definitions in his long chain of definitions in "On Formally Undecidable Propositions": > 45. x B y ≡ Bw(x) & [l(x)] Gl x = y > x is a proof of the formula y. > 46. Bew(x) ≡ (E y) y B x > x is a provable formula. [Bew(x) is the only one of the concepts 1-46 of which it cannot be asserted that it is recursive.] Here Gödel notes that all of his previous definitions that used existential quantifiers set an explicit limit for the size of the integer in question (there exists k such that k is less than or equal to ...), but definition 46 doesn't: it just says "there exists an integer y such that y is a proof of x" (according to Gödel numbering). If you did set a limit on the size of y then you would have a computable function, where the most naive implementation would be to just evaluate everything up to that size limit and check whether it is a valid proof of x (using Gödel's other formulas such as Bw). But it wouldn't match our overall notion of provability, because our notion of provability doesn't set any particular limit on the size of the proof.