# Re: is induction unformalizable?

```Wei Dai writes:
> 1. P=?NP is a purely mathematical problem, whereas the existence of an HPO
> box is an emperical matter. If we had access to a purported HPO box while
> P=?NP is still unsolved, we can use the box to exhaustively search for
> proofs of either P=NP or P<NP.```
```
I've seen many speculations that P=?NP may be undecideable under our
current axioms.  I guess this is because people are tired of looking
for proofs and PhD students don't want to get assigned this problem.

I'm not sure whether both of the following possibilities would be
consistent with the issue being undecideable:

A: There actually exists a polynomial-time algorithm to solve all
NP problems, but we can't prove that it always works, even though it
always does.

B: There is no polynomial time algorithm that solves all NP problems,
but we can't prove that no such algorithm exists.

I wonder if we could ask the HPO (halting problem oracle) box any harder
questions, that might help resolve the issue if it turned out that P=NP
is undecideable.  Could we use it to directly ask whether the algorithm
in case A above exists, and perhaps even to find it?

> 2. I think it's very unlikely that P=NP, but in case it is, we can still
> test an HPO box by generating random instances of hard problems with known
> solutions. (That is, you generate a random solution first, then generate a
> random problem with that solution in mind.) For example here's a page about
> generating random instances of the Traveling Salesman Problem with known
> optimal solutions.
>