What we envision is humans using informal reasoning and intuition as a powerful guide, with formal systems then verifying those ideas. In this way, the formal system grounds high-level intuition.