# Solving and Verifying the boolean Pythagorean Triples problem via Cube-and-Conquer

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

## Key facts

- Cited by 23 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 3 May 2016.

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

- [Inductive logic programming at 30](https://mlsanity.com/paper/2102.10556/) (2021)
- [Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning](https://mlsanity.com/paper/2502.13834/) (2025)
- [Answer Set Networks: Casting Answer Set Programming into Deep Learning](https://mlsanity.com/paper/2412.14814/) (2024)
- [Too much information: why CDCL solvers need to forget learned clauses](https://mlsanity.com/paper/2202.01030/) (2022)
- [AlphaMapleSAT: An MCTS-based Cube-and-Conquer SAT Solver for Hard Combinatorial Problems](https://mlsanity.com/paper/2401.13770/) (2024)
- [Learning Interestingness in Automated Mathematical Theory Formation](https://mlsanity.com/paper/2511.14778/) (2025)
- [Design of quantum optical experiments with logic artificial intelligence](https://mlsanity.com/paper/2109.13273/) (2021)
- [Inverting Cryptographic Hash Functions via Cube-and-Conquer](https://mlsanity.com/paper/2212.02405/) (2022)
- [Decomposing Hard SAT Instances with Metaheuristic Optimization](https://mlsanity.com/paper/2312.10436/) (2023)
- [From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificates](https://mlsanity.com/paper/2605.15445/) (2026)
- [Branching Strategy Selection Approach Based on Vivification Ratio](https://mlsanity.com/paper/2112.06917/) (2021)
- [SATViz: Real-Time Visualization of Clausal Proofs](https://mlsanity.com/paper/2209.05838/) (2022)
- [Artifical intelligence and inherent mathematical difficulty](https://mlsanity.com/paper/2408.03345/) (2024)
- [Smart Cubing for Graph Search: A Comparative Study](https://mlsanity.com/paper/2501.17201/) (2025)
- [Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimization](https://mlsanity.com/paper/2506.00674/) (2025)
- [Solver-Aided Expansion of Loops to Avoid Generate-and-Test](https://mlsanity.com/paper/2508.08442/) (2025)
- [Explaining Hitori Puzzles: Neurosymbolic Proof Staging for Sequential Decisions](https://mlsanity.com/paper/2508.14294/) (2025)
- [The Active Discoverer Framework: Towards Autonomous Physics Reasoning through Neuro-Symbolic LaTeX Synthesis](https://mlsanity.com/paper/2601.06117/) (2026)
- [Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discovery](https://mlsanity.com/paper/2604.21187/) (2026)
- [Learning Splitting Heuristics for Parallel String Solvers](https://mlsanity.com/paper/2606.20656/) (2026)
- [Streaming LRAT Certificates into Lean Theorems](https://mlsanity.com/paper/2607.00815/) (2026)
- [A Forced-Structure Reduction and Verifiable Bounds for Conway's 99-Graph](https://mlsanity.com/paper/2608.11211/) (2026)
- [The Refutation Gap: Certifying Both Halves of an Optimality Claim](https://mlsanity.com/paper/2609.20873/) (2026)

## Abstract (arXiv)

The boolean Pythagorean Triples problem has been a longstanding open problem in Ramsey Theory: Can the set N = 1, 2, ... of natural numbers be divided into two parts, such that no part contains a triple (a,b,c) with a2 + b2 = c2 ? A prize for the solution was offered by Ronald Graham over two decades ago. We solve this problem, proving in fact the impossibility, by using the Cube-and-Conquer paradigm, a hybrid SAT method for hard problems, employing both look-ahead and CDCL solvers. An important role is played by dedicated look-ahead heuristics, which indeed allowed to solve the problem on a cluster with 800 cores in about 2 days. Due to the general interest in this mathematical problem, our result requires a formal proof. Exploiting recent progress in unsatisfiability proofs of SAT solvers, we produced and verified a proof in the DRAT format, which is almost 200 terabytes in size. From this we extracted and made available a compressed certificate of 68 gigabytes, that allows anyone to reconstruct the DRAT proof for checking.