Mathematics solves problems by pen and paper. CS helps us to go far beyond that (cacm.acm.org)

Researchers report a new era in automated reasoning driven by modern SAT (satisfiability) solving and high-performance computing: enormous, completely automatic proofs—like the 200 TB verification of the Boolean Pythagorean Triples Problem—can now settle long-standing combinatorial questions that were previously out of reach. Using advanced SAT heuristics, parallel solvers (e.g., Cube-and-Conquer methods and the TREENGELING solver), and linear speedups across thousands of cores, they automatically found that the smallest n for which every 2‑coloring of {1,…,n} contains a Pythagorean triple is n = 7825; the analogous 3‑color case is provably >107. These results are generated by encoding problems into propositional logic and applying powerful paradigms such as Conflict‑Driven Clause Learning (CDCL) and look‑ahead splitting to systematically explore astronomically large search spaces. This development matters because it reframes “brute force” as “brute reasoning”: clever SAT algorithms turn exhaustive search into a practical tool for mathematics and for verification of complex hardware/software systems. Machine-generated proofs can be enormous but still checkable by trusted proof validators, so knowledge (correct answers) can trump human interpretability when safety and security demand certainty. The work highlights a tight feedback loop: hard combinatorial problems sharpen SAT techniques, and those techniques in turn unlock new mathematical and engineering guarantees that were previously infeasible.