Hilbert: Recursively Building Formal Proofs with Informal Reasoning

Sumanth Varambally, Thomas Voice, Yanchao Sun +3

Large Language Models (LLMs) demonstrate impressive mathematical reasoning abilities, but their solutions frequently contain errors that cannot be automatically checked. Formal the…