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 is no longer a Nash equilibrium and is a new Nash equilibrium which is also Pareto optimal.
- A fourth section on the biased strategic space and the "miracle move" .
Last updated: Dec 07 2023 at 16:21 UTC