Peter Scholze wants to rebuild much of modern mathematics, starting from one of its cornerstones. Now, he has received validation for a proof at the heart of his quest from an unlikely source: a computer.