# Learning dynamic polynomial proofs

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

## Key facts

- Cited by 8 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 4 Jun 2019.

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

- [A Survey on Deep Learning for Theorem Proving](https://mlsanity.com/paper/2404.09939/) (2024)
- [Evolving Scientific Discovery by Unifying Data and Background Knowledge with AI Hilbert](https://mlsanity.com/paper/2308.09474/) (2023)
- [AI Descartes: Combining Data and Theory for Derivable Scientific Discovery](https://mlsanity.com/paper/2109.01634/) (2021)
- [Self-Supervised Learning to Prove Equivalence Between Straight-Line Programs via Rewrite Rules](https://mlsanity.com/paper/2109.10476/) (2021)
- [Proving Equivalence Between Complex Expressions Using Graph-to-Sequence Neural Models](https://mlsanity.com/paper/2106.02452/) (2021)
- [Automated Proof of Polynomial Inequalities via Reinforcement Learning](https://mlsanity.com/paper/2503.06592/) (2025)
- [Foundation of Intelligence: Review of Math Word Problems from Human Cognition Perspective](https://mlsanity.com/paper/2510.21999/) (2025)
- [Learning to Coordinate Symbolic Tools: LLM Agents for Verified Sum-of-Squares Certificates](https://mlsanity.com/paper/2608.00326/) (2026)

## Abstract (arXiv)

Polynomial inequalities lie at the heart of many mathematical disciplines. In this paper, we consider the fundamental computational task of automatically searching for proofs of polynomial inequalities. We adopt the framework of semi-algebraic proof systems that manipulate polynomial inequalities via elementary inference rules that infer new inequalities from the premises. These proof systems are known to be very powerful, but searching for proofs remains a major difficulty. In this work, we introduce a machine learning based method to search for a dynamic proof within these proof systems. We propose a deep reinforcement learning framework that learns an embedding of the polynomials and guides the choice of inference rules, taking the inherent symmetries of the problem as an inductive bias. We compare our approach with powerful and widely-studied linear programming hierarchies based on static proof systems, and show that our method reduces the size of the linear program by several orders of magnitude while also improving performance. These results hence pave the way towards augmenting powerful and well-studied semi-algebraic proof systems with machine learning guiding strategies for enhancing the expressivity of such proof systems.