alt Hacker NewsUsing a proof language with an SMT solver is basically that: an inexplicable tick that it’s fine, until a small change is needed, the tick is gone, and nothing can say why.
Using a proof language with an SMT solver is basically that: an inexplicable tick that it’s fine, until a small change is needed, the tick is gone, and nothing can say why.
That's basically what sledgehammer (mentioned in the article) boils down to. The Lean folks use some safeguards to avoid issues with that, such as only using their "grind" at the end of a proof, where all the "building blocks" have been added to context.