The people who could instruct such AI and evaluate its outputs would be domain experts. Without them how would you even start to approach those problems?
Have you looked at the papers and C.V.s of the people on the front page of x.ai? Many have already worked on machine guided proofs and I see people with pure math and physics backgrounds.
Formal verification research is conducted since 30+ years and LLMs aren't really good at math and logic, so based on what grounds can we expect a breakthrough in machine guided proofs anytime soon?
cma|2 years ago
pms|2 years ago