A Formalization of the Generalized Quantum Stein's Lemma in Lean

Rodolfo Reis Soldati presents a Lean formalisation of a corrected proof of the generalised quantum Stein lemma, which gives relative entropy an operational interpretation in quantum resource theories. Formal verification combines topology, analysis and operator algebra, exposes small imprecisions in the mathematical argument and motivates a sharper definition of a resource theory. The resulting foundations extend the Lean-QuantumInfo library and support broader collaborative formalisation of quantum physics.