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.
@article{arxiv.2309.16224,
title = {Automatic Proof Checking and Proof Construction by Tactics},
author = {Gilles Dowek},
journal= {arXiv preprint arXiv:2309.16224},
year = {2023}
}