Lean Characteristic Set