Exact Matrix CompletionResearch Paper
Every time a streaming service guesses what you would rate a film you have never seen, it is solving a matrix completion problem: fill in the missing entries of a vast user-by-item table from the few that are observed. The question became famous during the Netflix Prize (2006-2009), and it looks hopeless - infinitely many matrices fit the observed entries - until one assumes the structure that makes recommendation possible: the table is essentially low rank, because tastes are governed by a few latent factors. In their landmark 2009 paper 'Exact Matrix Completion via Convex Optimization' (Foundations of Computational Mathematics), Emmanuel Candes and Benjamin Recht proved that an n-by-n matrix of rank r can be recovered exactly, with high probability, from only about n^1.2 * r * log n randomly observed entries - not by the NP-hard route of minimizing rank, but by minimizing the nuclear norm, a convex surrogate (the sum of the singular values) solvable efficiently. The proof, in the lineage of Candes-Romberg-Tao compressed sensing, turns on two ideas: an incoherence condition ensuring the singular vectors are spread out rather than spiky, and a dual certificate witnessing optimality, whose existence rests on delicate random-matrix concentration. It transformed a practical engineering puzzle into rigorous theory and seeded a decade of work across machine learning, signal processing, computer vision, and sensor localization. This mission formalizes the Candes-Recht exact-recovery theorem in Lean, decomposed into its dual-certificate construction and the probabilistic concentration reductions at its core.