# Learning to Prove Trigonometric Identities

arXiv: https://arxiv.org/abs/2207.06679 · HTML: https://mlsanity.com/paper/2207.06679/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 23 of its 56 references that are in the map.
- First posted on arXiv 14 Jul 2022.

## Builds on (most cited first, 23 of 23)

- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [Proximal Policy Optimization Algorithms](https://mlsanity.com/paper/1707.06347/) (2017)
- [Google's Neural Machine Translation System: Bridging the Gap between Human and Machine Translation](https://mlsanity.com/paper/1609.08144/) (2016)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [Generative Language Modeling for Automated Theorem Proving](https://mlsanity.com/paper/2009.03393/) (2020)
- [Analysing Mathematical Reasoning Abilities of Neural Models](https://mlsanity.com/paper/1904.01557/) (2019)
- [Deep Learning for Symbolic Mathematics](https://mlsanity.com/paper/1912.01412/) (2019)
- [End-to-End Differentiable Proving](https://mlsanity.com/paper/1705.11040/) (2017)
- [Visual Interpretability for Deep Learning: a Survey](https://mlsanity.com/paper/1802.00614/) (2018)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Interpretable Deep Learning: Interpretation, Interpretability, Trustworthiness, and Beyond](https://mlsanity.com/paper/2103.10689/) (2021)
- [Reinforcement Learning of Theorem Proving](https://mlsanity.com/paper/1805.07563/) (2018)
- [Graph Representations for Higher-Order Logic and Theorem Proving](https://mlsanity.com/paper/1905.10006/) (2019)
- [Premise Selection for Theorem Proving by Deep Graph Embedding](https://mlsanity.com/paper/1709.09994/) (2017)
- [INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving](https://mlsanity.com/paper/2007.02924/) (2020)
- [Learning to Prove Theorems by Learning to Generate Theorems](https://mlsanity.com/paper/2002.07019/) (2020)
- [TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learning](https://mlsanity.com/paper/2102.09756/) (2021)
- [Holophrasm: a neural Automated Theorem Prover for higher-order logic](https://mlsanity.com/paper/1608.02644/) (2016)
- [First Neural Conjecturing Datasets and Experiments](https://mlsanity.com/paper/2005.14664/) (2020)
- [Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling](https://mlsanity.com/paper/1911.06904/) (2019)
- [Learning to Prove from Synthetic Theorems](https://mlsanity.com/paper/2006.11259/) (2020)
- [ATPboost: Learning Premise Selection in Binary Setting with ATP Feedback](https://mlsanity.com/paper/1802.03375/) (2018)
- [A Survey on Theorem Provers in Formal Methods](https://mlsanity.com/paper/1912.03028/) (2019)

## Built on by (most cited first, 1 of 1)

- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)

## Abstract (arXiv)

Automatic theorem proving with deep learning methods has attracted attentions recently. In this paper, we construct an automatic proof system for trigonometric identities. We define the normalized form of trigonometric identities, design a set of rules for the proof and put forward a method which can generate theoretically infinite trigonometric identities. Our goal is not only to complete the proof, but to complete the proof in as few steps as possible. For this reason, we design a model to learn proof data generated by random BFS (rBFS), and it is proved theoretically and experimentally that the model can outperform rBFS after a simple imitation learning. After further improvement through reinforcement learning, we get AutoTrig, which can give proof steps for identities in almost as short steps as BFS (theoretically shortest method), with a time cost of only one-thousandth. In addition, AutoTrig also beats Sympy, Matlab and human in the synthetic dataset, and performs well in many generalization tasks.