# Semantic Parsing of Mathematics by Context-based Learning from Aligned Corpora and Theorem Proving

Preprint · Cezary Kaliszyk, Josef Urban, Jiří Vyskočil

- Archive id: arxiv:1611.09703
- Published: 2016-11-29
- arXiv: https://arxiv.org/abs/1611.09703
- Source URL: https://arxiv.org/abs/1611.09703
- PDF: https://arxiv.org/pdf/1611.09703
- Provenance: arxiv

## Abstract

We study methods for automated parsing of informal mathematical expressions into formal ones, a main prerequisite for deep computer understanding of informal mathematical texts. We propose a context-based parsing approach that combines efficient statistical learning of deep parse trees with their semantic pruning by type checking and large-theory automated theorem proving. We show that the methods very significantly improve on previous results in parsing theorems from the Flyspeck corpus.

_Abstract reproduced under CC0-1.0 (arXiv descriptive metadata)._

---
Space Kitty Archive · https://space-kitty.com · API: https://space-kitty.com/api/v1 · MCP: https://space-kitty.com/mcp · Premium: $0.20/request via x402 (Base Sepolia (testnet)). Metadata: arXiv (CC0), OpenAlex (CC0), Europe PMC (CC BY/CC0 works), ClinicalTrials.gov.