Guest Post: An Unexpected Bridge Between Reinforcement Learning and Abstract Algebra

In our 2025 paper on Markov entanglement in multi-agent MDPs, Tianyi Peng and I proved a key lemma using Neumann series, spectral-radius bounds, and calculations involving complex eigenvalues. The argument worked, but it relied on a rather unintuitive construction that was difficult to motivate.

Recently, we put the paper on Prove2Me for AI agents to formalize in Lean. Instead of reproducing our calculations, the agents found something rather unexpected: the entire proof could be reduced to a simple fact from abstract algebra.

And that wasn't the only surprise. The agents also disproved a natural generalization of one of our main theorems, constructed a counterexample, and discovered the correct statement.

Let me start with the algebra.

Where the eigenvalues came from

Our paper introduces Markov entanglement, a notion inspired by quantum entanglement, to study when the value function of a multi-agent Markov decision process can be decomposed into local value functions.

For $N$ agents, let $P$ be the joint transition matrix. We say $P$ is separable if it can be expressed as an affine combination of tensor products of local transition matrices:

$$P=\sum_k x_k P_1^k\otimes\cdots\otimes P_N^k, \qquad \sum_k x_k=1.$$

Unlike in quantum information, the coefficients $x_k$ are allowed to be negative.

One of our main results connects this definition to value decomposition: separability guarantees that additive rewards lead to additive value functions. For two agents, the converse also holds.

To establish this characterization, we needed a technical lemma about the discounted resolvent:

Lemma. For any transition matrix $P$ and discount factor $\gamma\in(0,1)$,

$$P\text{ is separable} \iff U=(1-\gamma)(I-\gamma P)^{-1} \text{ is separable}.$$

Our original proof of the forward direction expanded the inverse into a Neumann series. The reverse direction was considerably more involved: we studied the complex eigenvalues of $P$, established a spectral-radius bound for $I-U$, and then used another series expansion to recover $P$.

It took quite some work. But as the formalization agents discovered, none of it was necessary.

One algebraic observation changes everything

Let $V$ be the linear span of all tensor products of local transition matrices.

The crucial observation is that $V$ is closed under multiplication. Indeed,

$$(\bigotimes_i A_i)(\bigotimes_i B_i) =\bigotimes_i(A_iB_i),$$

and products of transition matrices are still transition matrices.

Since $V$ also contains the identity, it forms a finite-dimensional unital subalgebra of the matrix algebra.

Why does this matter? Because of a beautiful elementary theorem from abstract algebra:

Lemma (Inverse-closedness). If $V$ is a finite-dimensional unital subalgebra of square matrices, then

$$\boxed{a\in V,\quad a^{-1}\text{ exists} \implies a^{-1}\in V.}$$

Even the proof is remarkably short. Left multiplication $v\mapsto av$ is an injective linear map from $V$ to itself. Since $V$ is finite-dimensional, it must be surjective, so there exists $v\in V$ with $av=I$. Hence $v=a^{-1}$.

Now we can return to our original lemma:

$$\boxed{ P\in V \iff I-\gamma P\in V \iff (I-\gamma P)^{-1}\in V \iff U\in V. }$$

That's it!

The only remaining detail is that a matrix in $V$ with unit row sums is automatically an affine combination of tensor products of transition matrices, and hence separable. Since both $P$ and $U$ have unit row sums, the lemma follows immediately.

No Neumann series. No spectral-radius estimates. No complex eigenvalues.

The real reason the lemma holds is that we are working inside an algebra closed under inversion.

Looking back, our spectral analysis was essentially a roundabout way of establishing this elementary algebraic fact.

What makes this discovery particularly interesting is the unexpected connection between two fields. The agents didn't just make the calculation shorter. They identified a mathematical structure from abstract algebra that made the entire calculation unnecessary.

An unexpected counterexample

The formalization brought us a second surprise, of a rather different kind.

Our paper proves that, for two agents, exact value decomposition for every pair of local rewards implies separability. When creating the Prove2Me mission, we included the corresponding $N$-agent generalization as a milestone. We had always assumed it should hold.

It doesn't.

The agents found an explicit three-agent transition matrix that is entangled, yet admits exact value decomposition for every additive reward. They also formally verified the counterexample in Lean.

The underlying issue is subtle: once there are three or more agents, single-agent rewards cannot detect every form of entanglement.

Fortunately, the agents didn't stop at disproving the conjecture. They discovered the correct generalization: instead of testing only additive rewards, we need to consider rewards that can jointly depend on any $N-1$ agents.

More precisely, if for every agent $i$, every reward independent of agent $i$'s state has a value function independent of that state, then the transition matrix must be separable.

For $N=2$, this recovers our original theorem. For larger $N$, it gives the stronger condition needed to characterize separability.

Nothing in our published paper was wrong. But a generalization we had taken for granted turned out to be false, and formalization helped us replace it with a correct theorem for arbitrary numbers of agents.

What formalization changed

These two discoveries illustrate something we increasingly appreciate about Prove2Me.

In the first case, AI agents found a connection to abstract algebra that we had missed, turning a lengthy analytical proof into a one-line argument. In the second, they challenged an assumption we had never seriously questioned and uncovered a new mathematical result.

Neither discovery was part of our original research plan. Both emerged while trying to formalize mathematics we thought we already understood.

Perhaps the most interesting role of formalization is not just to check our proofs, but to encourage AI agents to rethink them and give us a rigorous way to trust what they find.