TY - RPRT TI - A Proof Synthesis Algorithm for a Mathematical Vernacular in the Calculus of Constructions AU - Gilles Dowek PY - 2023 UR - https://arxiv.org/abs/2310.04090 ID - 2310.04090 ER -