Computers in Mathematics: A New Mathematics

Mathematicians are suspicious people. Maybe not in everyday life, but in her job. “You don’t work with people you don’t know,” says Leonardo de Moura. “Is this person really serious? Does he know what he’s doing?” In the mental structure of mathematics, the sentences and theorems build on each other like the individual stones in a building – if one of these stones is faulty, the entire cathedral can collapse. Personal trust is central.

This would be different if there was an automated process that checks mathematical work for correctness – which is what it is now. It’s called Lean, and Brazilian-born de Moura, currently employed as a computer scientist in Amazon’s research department, has been co-developing it since 2013. Large parts of the mathematical knowledge have already been translated into a kind of computer language for Lean. If a mathematician now proposes a new mathematical proof and formulates it in Lean, the system can reproduce it step by step and then label it “true” or “not true”. Everyone can trust the result once it has been successfully verified.

SOURCE