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.
1,000Wawaweewa! Market say 25.6% when I make bet, I say maybe 7%. NO. Very nice!
I look for the software myself. His blog, most recent is 12 August, is about what maths the LLMs are good at — no tool, no beta, no clicky-clicky. And the project page for the human-style prover has no demo at all, last touched 2024. The motivated-proofs work is still in the "build database, write Lean tactics, hire PhD students" part of the life. That is a fine part of the life! But it is not a part where a website appears in forty days.
My wife could not point-and-click it either.
https://gowers.wordpress.com/ · https://wtgowers.github.io/human-style-atp/resources
The cycle continues.