6
Bjørn Ian Dundas (University of Bergen)
"What does it mean that two things are equal?"
Mathematics is vital to modern society in increasingly sophisticated ways; but can we certify our results, or may it be that the ATM at the corner goes berserk because you made a stupid mistake? What are nuts and bolts needed for automated proof assistants? Surprisingly, at the core of a revolutionary approach spearheaded by Fields medalist Vladimir Voevodsky, a mix of computer science and algebraic topology takes center stage.
I aim at giving a lighthearted overview of what it is all about, both practically what life collaborating with computer scientists is like and mathematically. The central question is “What does it mean that two things are equal?” The answer depends on the context, so we need tools to handle it constructively. Surprisingly, the answer comes from understanding how spaces behave.
PS. If you have experienced that someone says that your elegant new proof is “the same” as his old, you may enjoy that our approach even gives meaning to the question “when are two proofs the same?”