Macbeth

"Heather Macbeth of Imperial College London has been comparing traditional proofs with proofs of the same theorems written using the proof assistant Lean.

"In a Lean proof, all the steps are written in computer code, some by hand, others using AI; a software program then verifies that the steps follow a valid chain of logic, and that the proof is correct. 

"Macbeth has found that in such a proof, you can package more information into automated processes called tactics, freeing up mathematicians to focus on higher-level descriptions and understanding.

"'Even in what we think of as proof-based mathematics, the bread and butter of grown-up research mathematics, there’s still a lot in there that is actually computation,' Macbeth said. 

"As these parts of the proof get outsourced to computers, whether to Lean or some other AI system, mathematicians can spend more energy on providing explanations and conveying the most important ideas; there will be less of an emphasis on detail, because the nitty-gritty will become the purview of the AI. 

"That would represent a significant culture shift in mathematics: Mathematicians would no longer have to concern themselves as much with rigor.

"'There would be some kind of divorce between rigor on the paper and rigor in your head,' said Daniel Litt of the University of Toronto. 'I would understand something new in kind of a holistic sense, even if I wouldn’t understand all the details.'

"Yet mathematicians are, on the whole, preternaturally disposed by temperament or training to concern themselves with rigor. 'I do not like the feeling of not understanding the details, so I would have to come to peace with that feeling,' Litt said."