We'll discuss Lean verification, reliability, and related issues as they pertain to evaluating mathematics produced with/by AI.