If I can work through math proofs in an IDE with Lean helping check my work I might finally get around to diving into the higher level math I’ve always wanted to. Could open some doors to us working folks that don’t have an instructor to review our proof attempts.