Kaiyu Yang

Learning to Prove Theorems via Interacting with Proof Assistants

2019 · arXiv (Cornell University)

Humans prove theorems by relying on substantial high-level reasoning and problem-specific insights. Proof assistants offer a formalism that resembles human mathematical reasoning, representing theorems in higher-order logic and proofs as high-level tactics. However, human experts …