In this talk, you’ll learn why mathematical proof automation matters for both technology and humanity.

Mathematical proof automation is critical to moving applications such as ChatGPT beyond synthesising large pools of data to produce fluently written commentaries that may – or may not – be “true”. Advances in mathematical proof automation can deliver a paradigm shift, turning applications such as ChatGPT into something much more valuable than handy tools for automating research, sales and marketing campaigns.

However, by making it possible for applications to distinguish between falsehoods and accurate depictions of reality, mathematical proof automation also has far-reaching implications for humankind: are machines on the cusp of becoming “smarter” than people?