https://cordis.europa.eu/project/id/101083038/de
Realizing the Promise of Higher-Order SMT and Superposition for Interactive Verification | Nekoka |...
Proof assistants (also called interactive theorem provers) have a long history of being very tedious to use. The situation has improved markedly in the past...