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
Post a Comment