Silly question, but in Rocq, just for example, what does prevent you to fire `auto`, then, when it solves the goal, to just substitute it in your proof with the term that it constructed? Not calling you on BS, but genuinely interested in the problem
Making is knowing, it makes things intelligible. You only understand what you made or what you know how to make. This is the foundation of epistemology of the Napolitan philosopher Giambattista Vico, and it explains why we lose the knowledge of software faster than it decays technically. The post overviews Vico's philosophy from a viewpoint of a system/software engineer and lists concerns about AI code generation.