This is an issue that has already come up to some extent. The initial proof of the Robbins conjecture used automated proving systems for a large amount of it, and they made no intuitive sense. It took about 2 years for someone to grok the proof well enough to present a version that made sense to people.
This is an issue that has already come up to some extent. The initial proof of the Robbins conjecture used automated proving systems for a large amount of it, and they made no intuitive sense. It took about 2 years for someone to grok the proof well enough to present a version that made sense to people.