A formal verification of the low-degree test, part of the proof of MIP* = RE, in Lean 4 using Mathlib.
Based on the paper: Quantum soundness of the classical low individual degree test by Ji, Natarajan, Vidick, Wright, and Yuen (2020).
A formal verification of the low-degree test, part of the proof of MIP* = RE, in Lean 4 using Mathlib.
Based on the paper: Quantum soundness of the classical low individual degree test by Ji, Natarajan, Vidick, Wright, and Yuen (2020).