Digital underpinnings for the logical

Everyone knows that 2 + 2 = 4. “But it is not enough to just know it or take it for granted,” explains Jasmin Blanchette, Professor of Theoretical Computer Science and Theorem Proving at LMU since March. “You have to be able to prove it logically.” Blanchette’s discipline explores the very bedrock of computer science: how abstraction and modeling are used to structure, process, transmit and reproduce information. Specifically, he concerns himself with technology-assisted theorem proving. “A theorem is a true logical statement or equation that can be proven,” he says. And computer programs known as ‘theorem provers’ have already been supporting this process for a number of years. “My research,” the professor adds, “seeks to reinforce automated proving and make it more cost-effective.”

A native of Canada, Blanchette studied computer science at the University of Sherbrooke in his home country and in Oslo. His doctoral thesis at the Technical University of Munich (TUM) already focused on theorem provers. His subsequently research began at TUM and was followed by stints at Inria in Nancy, France, and at the Max Planck Institute for Informatics in Saarbrücken. He also worked for a Norwegian software company. 2017 brought a move to the Vreie Universiteit (VU) Amsterdam before he took up his appointment at LMU in 2023.

“A bit like looking for typos”

A hallmark of Blanchette’s research is the combination of automated and interactive proving programs. “In the former case, the technology examines the logic fully automatically. In the latter case, the user takes the first step in the chain of evidence in a kind of text editor.” One classic mathematical move at this point is referred to as ‘induction via x’: The program proposes multiple subsets for which it then searches for proof, effectively ‘at the push of a button” by the user. “If that doesn’t work, the user has to intervene again by specifying a different induction, simplifying the sentence or tweaking something or other.” The automated provers that Blanchette uses and develops himself in his research are text-based: “They are similar to programming languages like Mathematica. If one link in the chain is not correct, that gets flagged – a bit like the way Word underscores typos in red.”

Blanchette is co-developer of interactive theorem provers such as ‘Isabelle’, which he has been working on since earning his doctorate at TUM. He is also involved in developing a fully automated prover. The relative reliability of the prover programs is attributable to what is known as their ‘small core’, which generates all subordinate proofs. “These programs have only a couple of thousand lines of codes, so they are very manageable for computer scientists. Manual reading and checking is easy,” the researcher says. “All complicated proofs are thus reduced to small steps – to straightforward core proofs.” If the core is too big, its output can be reviewed using a different, external approach: “So, we use a second proving program to check the output of the first.”

Most people who use this kind of proof assistant are themselves computer scientists. “They help informatics experts to save time, because it is not easy to produce extensive proofs by hand.” On the other hand, the programs can help mathematicians to substantiate manual proofs for complex theorems, shorten chains of evidence or generally come up with better proving strategies.

Security software and the existence of God

“Even philosophers use the automated provers to some extent – when addressing the existence of God, for example. Some computer linguists use them, too.” One important application in industry is the verification of security-related software. Accordingly, Blanchette also cooperates with chairs of informatics at LMU that concern themselves with this topic.

Going forward, the professor would like to see automated provers deployed as a matter of routine for critical computer infrastructures, to draft programming languages and, more generally, to advance research in both computer science and mathematics. His hope is that this will lead to “more trustworthy systems and research outcomes”. The use of artificial intelligence in the search for proof is already trending in this direction.

Yet however sophisticated the mathematics, however many thousands of lines of code you have, however much AI you deploy, “You can never be a hundred percent certain that something is true,” Blanchette asserts, “not even with 2 + 2 = 4. Because – in purely logical terms – that is ultimately impossible.”