Can AI give formal proof to prove theorem which is not proven (formally by human) yet such as “Every planar graph is 4 colorable”?

I am not talking about current AI models (those which are insuffiecient to solve open problems) but in future is it possible to develop such AI models?

I tried to solve using chatGPT but it keep saying that “This is conjecture/open problem/etc and have no formal proof.”