Comment by bagels

"we aim to tackle the challenges of scalability, usability, and proof (Mathematics) automation in the Lean proof assistant."