The heritage of most proof assistants was "AI" too.
Conversation
This is a very notable difference between proof assistant cultures, also -- much more AI heritage in Isabelle than in Coq for example.
2
5
How so?
1
For one thing, Isabelle's emphasis on automation and Coq's emphasis on inductive structures reflects the research interests of the people who made it.
2
5
Yeah true. TBH I think automation is often much easier in constructive logics, and the fact that classical proof assistants are more automated is an artifact of history
2
1
I don't know why you say that, but I'd be willing to be convinced. The main source of great automation in Isabelle is the ability to rewrite by thousands of equalities, and therefore the very flexible notion of equality in Isabelle that supports e.g. quotients
3
4
You get the same exact thing out of path equality in cubical, but nobody who likes cubical cares about automation
2
1
Cubical + e-graphs boom you're done
4
1
Can e-graphs be done fast? I looked at them a bit but it seemed they were taking a pretty slow approach to name binding/substitution. Would be cool to figure out how to get e-graphs to work with the semantic type checking stuff - is that possible at all?
2
2
I think keeping them efficient will be one of (the only? once a type theorist is involved) the challenges of adapting them to cubical
1
1
Neat - yeah I would love to see this stuff support fast, interactive editing, which is why I'm interested!