Post #2438863

@tao@mathstodon.xyz you mentioned earlier that for more elaborate proofs a human would still have to guide the process and provide a high level Ansatz. I imagine that the person who controls the system in such a context will already need to digest the proof to be an effective guide.