On the contrary proof assistants help one systematize and organize existing concepts. They are a great way to revise the basic curriculum and revolutize pedagogy. They make the creative process of defining new mathematical objects more accessible, and easier to motivate via unlocking more code reuse. They are a great way to revise the basic curriculum and revolutize pedagogy.