PSI researchers used an AI system to solve five open problems in quantum information theory. Each result includes a paper, a Lean formalization and verification code. The release repository documents how AI contributed to each proof. One result sets a new three-copy threshold for distilling Bell pairs from Werner states. Another proves CHSH Bell inequality violations cannot occur beyond a finite separation in vacuum correlations. A third identifies Fourier-phase measurements as optimal for Bell inequality violations. A fourth shows 2(d−1) positive-partial-transpose maps suffice to break entanglement in d-dimensional systems. The fifth provides a counterexample to the claim that all causal processes can arise from larger finite-dimensional reversible processes.