Automatic Proof Checking and Proof Construction by Tactics
arXiv:2309.16224
Abstract
In this note we compare two kinds of systems that verify the correctness of mathematical developments: roof checking and proof construction by tactics and we propose to merge them in a single system.