Tim Gowers Talking About Human-Oriented Automated Theorem Proving

See Tim Gowers and Norman Wildberger Playing With Robots.

This was earlier today, from the 2025 Big Proof workshop at the Isaac Newton Institute:

They wrote a program called ROBOT that printed out proofs as if written by a human being. See A fully automatic problem solver with human-style output by M. Ganesalingam and W. T. Gowers. See also his 2022 blog post: Announcing an automatic theorem proving project. He says (21:30) he was initially thinking it would be GOAT-Oriented Automated Theorem Proving but that he has since scaled back the expectation. cf the Grand Canonical Blueprint in More Robotics with Terence Tao. (49:15) These "Rabbits out of a Hat" moments occur when there is a more efficient way to arrange the theory.

Emily Riehl's talk Formalizing invisible mathematics: case studies from higher category theory was on Monday:

Well, since she apparently asked for it (3:14): see Andrej Bauer's "Five Stages of Accepting Constructive Mathematics".

Subscribe to INI Seminar Room 1.


Marcus du Sautoy - Blueprints: how mathematics shapes creativity

That's his new book: Blueprints: How mathematics shapes creativity.

I think it should work both ways: see Dmitri Tymoczko - Symmetry and Complexity in Music.

Subscribe to Oxford Mathematics.

Comments

Popular posts from this blog

Steven Johnson - So You Think You Know How to Take Derivatives?

Welsh Republic Podcast Talking With Kars Collective on Armenia Azerbaijan Conflict

Hitachi HD44780U LCD Display Fonts