2 papers
cs.AI2025
Learning Conjecturing from Scratch
Thibault Gauthier, Josef Urban
We develop a self-learning approach for conjecturing of induction predicates on a dataset of 16197 problems derived from the OEIS. These problems are hard for today's SMT and ATP s…
cs.LO2024
A Formal Proof of R(4,5)=25
Thibault Gauthier, Chad E. Brown
In 1995, McKay and Radziszowski proved that the Ramsey number R(4,5) is equal to 25. Their proof relies on a combination of high-level arguments and computational steps. The author…