Partition Principle ($PP$) is the following statement:
For all sets $a$, $b$ there is an injection $f:a\rightarrow b$ iff there is a surjection $g:b\rightarrow a$
It is known that $ZF\vdash AC\rightarrow PP$ but as far as I know it is still open that $ZF\vdash PP\rightarrow AC$.
Question 1: What are references for partial results on proving or refuting $ZF\vdash PP\rightarrow AC$?
Let's assume this conjecture is false. Then the main question is:
How to prove $Con(ZF)\Longrightarrow Con(ZF+PP+\neg AC)$?
Miller has a construction for $Con(ZF)\Longrightarrow Con(ZF+\neg AC)$ using a special inner model of $ZF$ in a generic extension. The main idea of this construction is based on the following facts:
Definition: Let $M$ be a ground model and $K$ an inner model of $ZF$ (not necessarily a model of $ZFC$) definable in any model of $ZF$. The pair of forcing notions $\mathbb{P}, \mathbb{Q}$ in $M$ have Miller Property over inner model $K$ iff for all formula $\varphi(x)$ and for all $\alpha\in o(M)$ we have
$$1\Vdash_{\mathbb{P}}(\varphi(\alpha^{\vee}))^K~~~\text{iff}~~~1\Vdash_{\mathbb{Q}}(\varphi(\alpha^{\vee}))^K$$
Which $\alpha^{\vee}$ is the canonical name of $\alpha$ in $M$.
Fact 1: For $I,J$ uncountable in $M$, the forcing notions $Fn(I,2)$ and $Fn(J,2)$ have Miller property over inner model $L(P(\omega))$ of $ZF$.
Fact 2: Using forcing notions like what we introduced in step 1, one can build a generic extension $M[G]$ such that $(L(P(\omega)))^{M[G]}\models ZF+\neg AC$ and the fact that $(L(P(\omega)))^{M[G]}\models \neg AC$ comes from Miller Property of the special type of forcing notions which we used.
Question 2: Is it possible to find a reformulation of Miller's construction to prove consistency of Partition Principle and negation of Axiom of Choice? For example, may something similar to the following approach work? If not, what is wrong?
Step 1: Finding some inner model $K$ such that $K\models ZF+PP$
Question 3: What are examples of such inner models? Surely in this case I am searching for inner models of $ZF$ that doesn't satisfy $AC$ necessarily. (e.g. $L(P(\omega))$) But the point is that finding such an inner model doesn't complete the proof because the situation of $AC$ in this inner model depends on its background model which is a generic extension of a ground model ($M[G]$). Thus one should go to another step by building an appropriate background model using a nice forcing notion over a nice ground model ($M$) which possibly contains something more than merely $ZF$. Perhaps it should satisfy some large cardinal axioms too.
Step 2: Finding some type of forcing notions which have Miller Property on inner model $K$.
Step 3: Forcing with this type of forcing notions and considering $K^{M[G]}$ which is a model of $ZF+PP$
Step 4: Proving $K\models \neg AC$ using Miller Property of forcing notions.
Best Answer
Yes, currently the problem is open whether or not the Partition Principle and the Axiom of Choice are equivalent. There are two major factors for this (in my opinion):
Many people become less interested in choiceless results. So while they might be very happy to hear about them, they prefer to put their research efforts towards other directions.
The Partition Principle gives us just enough structure on the cardinals so the obvious approaches fail pretty fast; but it also indicates that the failure of the axiom of choice might be far away from the ordinals. In other equivalences we can usually show that if a principle fails somewhere, then it will often fail on something which is "close to the ordinals" in some sense.
This is a vague statement, and I don't intend to clarify on it further. To understand it, feel free to try and apply some of the usual approaches to this problem.
Forcing. Forcing is a great tool for proving consistency results. The "Miller property" which is better described as absoluteness, is not the reason why $L(\Bbb R)$ fails to satisfy the axiom of choice. This is actually not that difficult, once you add "enough" reals which "look the same" you can easily confuse the axiom of choice in a model like $L(x)$ where $x$ is any set including sufficiently many reals.
This was observed by Feferman/Solovay a long time ago. If you add $\omega_1$ Cohen reals to $L$, then $L(\Bbb R)$ fails to satisfy the axiom of choice (but it does satisfy the principle of dependent choice).
But models of the form $L(x)$ will almost usually fail to satisfy the partition principle if the axiom of choice fails. For example there is a definable surjection from $\Bbb R$ onto $\omega_1$; but if there are not $\omega_1$ sequences of reals in $L(x)$ then there is no injection back. Another example is that if there is an infinite Dedekind-finite set, then there is one which can be mapped onto $\omega$, but by definition there will be no injection in the other direction.
And this is true in many of these constructions of inner models of generic extensions. We will usually be able to single out that the set we are interested in has this sort of property which witnesses the failure of the Partition Principle.
So what about forcing? Forcing works fine without the axiom of choice. But we are so used to thinking about it in terms of the axiom of choice, that it becomes very difficult to use forcing as arbitrarily as we do when choice fails. We lose the ability to talk about chain conditions (because some forcings don't have maximal antichains at all), the mixing lemma can fail, and closure does not imply distributivity.
Then when we force over models where the axiom of choice fails we lose the ability to use these tools, and again we can often find examples which are either very hard to understand (so we don't know much about them yet), or witness the catastrophes which may befall on us (we may add unintentional real numbers in the process, and so on and so forth).
So we can try and appeal to absoluteness, but this will usually work for forcings which are associated with ordinals, forcings which are well-ordered inherently (like collapsing something to $\omega$) or has sufficiently "pretty" structure. Not to mention that if the Principle fails, it can fail in many places, which would require you to work much harder than you would have. There is a reason why so little people throughout history understood Sageev's proof for "For all infinite $a$, $a+a=a$ does not imply the axiom of choice". It's a monumentally difficult proof which is spanned over 180 pages (and that's an edited version of his Ph.D.)
So what can we do? Not much currently. As I wrote in the comment, I find this problem to be a lighthouse in the bogs of mathematics. I think to myself what sort of thing would have helped me to prove such a result. But there is a huge distance from my ideas to implementations, and even when the tools I currently craft will be ready for use, it might still take a long time before I will have any idea on how to apply them properly to this problem.