Nivat Conjecture Proposed for DeepMind's Formal Conjectures Project... Highlighting Frontier Models' Ability to Synthesize Approaches

According to the original text, AI is playing a role in breaking the limitations of existing systems. Frontier models are skilled at synthesizing different mathematical approaches and can find connections through notation conversion, comparison of partial results, and trying thousands of combinations. In this context, the Nivat Conjecture was proposed for inclusion in Google DeepMind's Formal Conjectures project. This served as an opportunity to make the problem a target for automated reasoning and to draw more attention to this question.