To recap for potential newcomers: Yijun and I have completed the formalizations of the no-cloning theorem and of the quantum teleportation algorithm :tada:

@Yijun He is formalizing the quantum Fourier transform in his fork.

@Hanna Lachnitt is formalizing Deutsch's algorithm in her fork.

Deutsch's algorithm is complete :party_ball: Next is Deutsch-Jozsa.

@Hanna Lachnitt Congrats! :+1:

I will have a look at your file as soon as possible.

Thanks to @Hanna Lachnitt The Deutsch-Jozsa algorithm is now part of the library.

Thanks to @Yijun He and @Hanna Lachnitt the quantum prisoners's dilemma is now part of the library.

However, much remains to be done:

- Formal specifications for Nash equilibrium and Pareto optimum in the context of the`locale restricted_strategic_space`

, then prove that in the maximally entangled case $D \otimes D$ is no longer a Nash equilibrium and $Q \otimes Q$ is a new Nash equilibrium which is also Pareto optimal.

- A fourth section on the biased strategic space and the "miracle move" $M$.

Last updated: Dec 07 2023 at 16:21 UTC