What role is there, if any, for human-oriented automatic theorem proving today?

Add to your list(s) Download to your calendar using vCal

• William Timothy Gowers (University of Cambridge)
• Friday 13 June 2025, 09:15-10:15
• Seminar Room 1, Newton Institute.

If you have a question about this talk, please contact nobody.

BPRW03 - Big proof: formalizing mathematics at scale

Human-oriented theorem proving is the approach to automatic theorem proving that seeks to create algorithms that find proofs in a way that is modelled as closely as possible on how humans find them. It used to be contrasted with machine-oriented theorem proving, where the emphasis was far more on exploiting to the full the vastly superior speed and memory of computers. At the last Big Proof meeting I argued that despite the fact that the machine-oriented approach was more fashionable, it was important not to lose sight of the human-oriented approach. Since that meeting, the whole discussion has been greatly changed by the dramatic developments in AI. I shall argue, but more tentatively, that it is still worth investing significant effort into understanding how human mathematicians find proofs. I shall also report on some of the work my group in Cambridge has been doing in that direction.

This talk is part of the Isaac Newton Institute Seminar Series series.

This talk is included in these lists:

• All CMS events
• Featured lists
• INI info aggregator
• Isaac Newton Institute Seminar Series
• School of Physical Sciences
• Seminar Room 1, Newton Institute
• bld31

Note that ex-directory lists are not shown.