# TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Models

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

## Key facts

- Cited by 24 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 27 of its 57 references that are in the map.
- First posted on arXiv 16 Oct 2023.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

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

- [Adam: A Method for Stochastic Optimization](https://mlsanity.com/paper/1412.6980/) (2014)
- [GPT-4 Technical Report](https://mlsanity.com/paper/2303.08774/) (2023)
- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Self-Refine: Iterative Refinement with Self-Feedback](https://mlsanity.com/paper/2303.17651/) (2023)
- [Are NLP Models really able to Solve Simple Math Word Problems?](https://mlsanity.com/paper/2103.07191/) (2021)
- [LeanDojo: Theorem Proving with Retrieval-Augmented Language Models](https://mlsanity.com/paper/2306.15626/) (2023)
- [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)
- [Inter-GPS: Interpretable Geometry Problem Solving with Formal Language and Symbolic Reasoning](https://mlsanity.com/paper/2105.04165/) (2021)
- [Analysing Mathematical Reasoning Abilities of Neural Models](https://mlsanity.com/paper/1904.01557/) (2019)
- [Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofs](https://mlsanity.com/paper/2210.12283/) (2022)
- [Autoformalization with Large Language Models](https://mlsanity.com/paper/2205.12615/) (2022)
- [HyperTree Proof Search for Neural Theorem Proving](https://mlsanity.com/paper/2205.11491/) (2022)
- [Formal Mathematics Statement Curriculum Learning](https://mlsanity.com/paper/2202.01344/) (2022)
- [The Lean mathematical library](https://mlsanity.com/paper/1910.09336/) (2019)
- [Proof Artifact Co-training for Theorem Proving with Language Models](https://mlsanity.com/paper/2102.06203/) (2021)
- [Learning to Prove Theorems via Interacting with Proof Assistants](https://mlsanity.com/paper/1905.09381/) (2019)
- [LEGO-Prover: Neural Theorem Proving with Growing Libraries](https://mlsanity.com/paper/2310.00656/) (2023)
- [Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Provers](https://mlsanity.com/paper/2205.10893/) (2022)
- [Generate & Rank: A Multi-task Framework for Math Word Problems](https://mlsanity.com/paper/2109.03034/) (2021)
- [NaturalProofs: Mathematical Theorem Proving in Natural Language](https://mlsanity.com/paper/2104.01112/) (2021)
- [FIMO: A Challenge Formal Dataset for Automated Theorem Proving](https://mlsanity.com/paper/2309.04295/) (2023)
- [LIME: Learning Inductive Bias for Primitives of Mathematical Reasoning](https://mlsanity.com/paper/2101.06223/) (2021)
- [INT: An Inequality Benchmark for Evaluating Generalization in Theorem Proving](https://mlsanity.com/paper/2007.02924/) (2020)
- [Learning to Reason in Large Theories without Imitation](https://mlsanity.com/paper/1905.10501/) (2019)
- [Lyra: Orchestrating Dual Correction in Automated Theorem Proving](https://mlsanity.com/paper/2309.15806/) (2023)

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

- [From System 1 to System 2: A Survey of Reasoning Large Language Models](https://mlsanity.com/paper/2502.17419/) (2025)
- [Towards Large Reasoning Models: A Survey of Reinforced Reasoning with Large Language Models](https://mlsanity.com/paper/2501.09686/) (2025)
- [DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Data](https://mlsanity.com/paper/2405.14333/) (2024)
- [OptiBench Meets ReSocratic: Measure and Improve LLMs for Optimization Modeling](https://mlsanity.com/paper/2407.09887/) (2024)
- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Can LLM Graph Reasoning Generalize beyond Pattern Memorization?](https://mlsanity.com/paper/2406.15992/) (2024)
- [Process-Driven Autoformalization in Lean 4](https://mlsanity.com/paper/2406.01940/) (2024)
- [MUSTARD: Mastering Uniform Synthesis of Theorem and Proof Data](https://mlsanity.com/paper/2402.08957/) (2024)
- [Proving Theorems Recursively](https://mlsanity.com/paper/2405.14414/) (2024)
- [FormalAlign: Automated Alignment Evaluation for Autoformalization](https://mlsanity.com/paper/2410.10135/) (2024)
- [PDE-Controller: LLMs for Autoformalization and Reasoning of PDEs](https://mlsanity.com/paper/2502.00963/) (2025)
- [Measuring Social Norms of Large Language Models](https://mlsanity.com/paper/2404.02491/) (2024)
- [UNComp: Can Matrix Entropy Uncover Sparsity? -- A Compressor Design from an Uncertainty-Aware Perspective](https://mlsanity.com/paper/2410.03090/) (2024)
- [Measuring Vision-Language STEM Skills of Neural Models](https://mlsanity.com/paper/2402.17205/) (2024)
- [Adapting Large Language Models for Education: Foundational Capabilities, Potentials, and Challenges](https://mlsanity.com/paper/2401.08664/) (2023)
- [MMSciBench: Benchmarking Language Models on Chinese Multimodal Scientific Problems](https://mlsanity.com/paper/2503.01891/) (2025)
- [A Hybrid RAG System with Comprehensive Enhancement on Complex Reasoning](https://mlsanity.com/paper/2408.05141/) (2024)
- [From Hypothesis to Publication: A Comprehensive Survey of AI-Driven Research Support Systems](https://mlsanity.com/paper/2503.01424/) (2025)
- [Understanding the Mixture-of-Experts with Nadaraya-Watson Kernel](https://mlsanity.com/paper/2509.25913/) (2025)
- [SwingArena: Competitive Programming Arena for Long-context GitHub Issue Solving](https://mlsanity.com/paper/2505.23932/) (2025)
- [SAS: Simulated Attention Score](https://mlsanity.com/paper/2507.07694/) (2025)
- [Self-Adjust Softmax](https://mlsanity.com/paper/2502.18277/) (2025)
- [ATTS: Asynchronous Test-Time Scaling via Conformal Prediction](https://mlsanity.com/paper/2509.15148/) (2025)
- [G"odel's Poetry](https://mlsanity.com/paper/2512.14252/) (2025)

## Abstract (arXiv)

Automated theorem proving (ATP) has become an appealing domain for exploring the reasoning ability of the recent successful generative language models. However, current ATP benchmarks mainly focus on symbolic inference, but rarely involve the understanding of complex number combination reasoning. In this work, we propose TRIGO, an ATP benchmark that not only requires a model to reduce a trigonometric expression with step-by-step proofs but also evaluates a generative LM's reasoning ability on formulas and its capability to manipulate, group, and factor number terms. We gather trigonometric expressions and their reduced forms from the web, annotate the simplification process manually, and translate it into the Lean formal language system. We then automatically generate additional examples from the annotated samples to expand the dataset. Furthermore, we develop an automatic generator based on Lean-Gym to create dataset splits of varying difficulties and distributions in order to thoroughly analyze the model's generalization ability. Our extensive experiments show our proposed TRIGO poses a new challenge for advanced generative LM's including GPT-4 which is pre-trained on a considerable amount of open-source formal theorem-proving language data, and provide a new tool to study the generative LM's ability on both formal and mathematical reasoning.