According to this recent blog https://gowers.wordpress.com/2025/09/22/creating-a-database-of-motivated-proofs/

Sir Gowers has been working on a motivated proof database and system to generate new ones (with the hope of training better LLMs). Will I be able to use a point-and-click motivated proof generator, released by Gower's team, by market close?

Resolves YES if such a website or program is freely available, or if I happen to be given beta access at any point before or including market end date. Resolves NO if they do not release or I am otherwise prevented from access, even if someone outside the Gower's team completes a version of the project.

Creating a database of motivated proofs

It's been over three years since my last post on this blog and I have sometimes been asked, understandably, whether the project I announced in my previous post was actually happening. The answer is yes -- the grant I received from the Astera Institute has funded several PhD students and a couple of postdocs, and…