Moa Johansson is an associate professor at Chalmers University in Gothenburg, Sweden. She’s interested in AI applied to mathematics and reasoning about functional programs.
How do you know that a mathematical proof is correct? And how do we find a nice elegant proof in the first place? Can computers help us with this? Solving mathematical problems was in fact one of the tasks adressed by the earliest AI systems developed already in the 1950’s. In this talk I will give a brief history of computer mathematics and how it connects to the development of early functional programming languages like Standard ML. I will also talk about some of my current research in how we can get computers to act creatively in the domain of mathematics; not only reason about given facts, as historically has been the case, but also invent and prove new interesting facts. To achieve this, we use tools like Haskell’s QuickCheck to allow our system, Hipster, to explore and test its way towards promising conjectures.
Slides