For example, let's consider a Math word problem like "On dividing 2272 and 875 by a 3-dight number N, we get the same remainder. Find N (and the sum of its digits).". AI could give us a solution but do we know if the solution is right and more importantly, do we know if it is a solution to the original problem? Since this is a Math example, a proof assistant like Lean can prove the former, but the latter (mapping the Math problem in English to Lean constraints) is unsolved. It is stuck in the same bucket as LLMs as a judge is currently - i.e. ML models with bounded accuracy. Ultimately, human expert(s) alone would be able to vet the solution and benefit from it, especially for problems more complicated than high school Math.