Proof assistants like Lean are there to catch any errors. Now, can you just feed the error logs back to the AI and let it iteratively fix any mistakes? I don't know, I haven't used those things in two decades.

Laymen understand very little about the how the world works at the most fundamental level even with all the resources in the world.

For example there’s enough information available to know what you’re describing but the people with the IQ, time, access, ability - basically asymptote to zero for anything more complicated than cleaning a house.