mlsanityData to 7 Oct 2026

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

arXiv 1605.00723 ↗First posted 3 May 2016cs.DM cs.LOcited by 23

Not on the map. Why?

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.

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

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2021: 3; 2022: 3; 2023: 1; 2024: 3; 2025: 6; 2026: 7.

23 papers.

Sort:

By area:

  1. 2021Inductive logic programming at 30cited by 46
  2. 2025Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoningcited by 17
  3. 2024Answer Set Networks: Casting Answer Set Programming into Deep Learningcited by 6
  4. 2022Too much information: why CDCL solvers need to forget learned clausescited by 2
  5. 2024AlphaMapleSAT: An MCTS-based Cube-and-Conquer SAT Solver for Hard Combinatorial Problemscited by 2
  6. 2025Learning Interestingness in Automated Mathematical Theory Formationcited by 2
  7. 2021Design of quantum optical experiments with logic artificial intelligencecited by 1
  8. 2022Inverting Cryptographic Hash Functions via Cube-and-Conquercited by 1
  9. 2023Decomposing Hard SAT Instances with Metaheuristic Optimizationcited by 1
  10. 2026From LLM-Generated Conjectures to Lean Formalizations: Automated Polynomial Inequality Proving via Sum-of-Squares Certificatescited by 1
  11. 2021Branching Strategy Selection Approach Based on Vivification Ratiocited by 0
  12. 2022SATViz: Real-Time Visualization of Clausal Proofscited by 0
11 more
  1. 2024Artifical intelligence and inherent mathematical difficultycited by 0
  2. 2025Smart Cubing for Graph Search: A Comparative Studycited by 0
  3. 2025Thinking Out of the Box: Hybrid SAT Solving by Unconstrained Continuous Optimizationcited by 0
  4. 2025Solver-Aided Expansion of Loops to Avoid Generate-and-Testcited by 0
  5. 2025Explaining Hitori Puzzles: Neurosymbolic Proof Staging for Sequential Decisionscited by 0
  6. 2026The Active Discoverer Framework: Towards Autonomous Physics Reasoning through Neuro-Symbolic LaTeX Synthesiscited by 0
  7. 2026Doubly Saturated Ramsey Graphs: A Case Study in Computer-Assisted Mathematical Discoverycited by 0
  8. 2026Learning Splitting Heuristics for Parallel String Solverscited by 0
  9. 2026Streaming LRAT Certificates into Lean Theoremscited by 0
  10. 2026A Forced-Structure Reduction and Verifiable Bounds for Conway's 99-Graphcited by 0
  11. 2026The Refutation Gap: Certifying Both Halves of an Optimality Claimcited by 0